1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
|
\begin{theindex}
\item {{\ptt !} (assumption prefix)}, 6
\item {{\ptt <==} (backward implication)}, \see{{\ptt PMI\_DEF}}{2}
\item {{\ptt ?} (conjecture prefix)}, 12
\item {{\ptt @} (bad conjecture prefix)}, 12
\item {{\ptt \$} (used conjecture prefix)}, 12
\item {{\ptt |} (lemma prefix)}, 10
\indexspace
\item {\ptt add\_relation}, 20--21, 25
\item {\ptt ADD\_SUPPOSE}, 12, 26
\item {\ptt add\_suppose}, 26
\item {\ptt ADD\_THEOREM}, 10, 27
\item {\ptt add\_theorem}, 27
\item {\ptt add\_weak}, 21, 28
\item {\ptt all\_hypotheses}, 40
\item {\ptt ALL\_STACKS}, 14, 30
\item applicable, 12
\item {\ptt APPLY\_TRANSFORM}, 16, 30
\item {\ptt ASM\_REWRITE\_WIN}, 30
\item {\ptt asm\_rewrite\_win}, 31
\item assumptions, 6
\indexspace
\item {\ptt BAD\_CONJECTURES}, 13, 31
\item {\ptt BEGIN\_STACK}, 6--7, 14, 32
\item {\ptt BEGIN\_STACK\_TAC}, 16, 33
\item {\ptt bound}, 34
\indexspace
\item {\ptt CB}, 16
\item {\ptt CLOSE\_STACK\_TAC}, 16
\item {\ptt CLOSE\_WIN}, 9, 35
\item {\ptt CONJECTURE}, 12, 36
\item {\ptt conjecture}, 37
\item conjectures, 12
\subitem bad, 12
\subitem used, 12
\item {\ptt conjectures}, 37
\item {\ptt context}, 38
\item {\ptt CONVERT\_WIN}, 8, 38
\item {\ptt convert\_win}, 39
\item {\ptt create\_win}, 39
\item {\ptt CURRENT\_NAME}, 14, 40
\indexspace
\item {\ptt dest\_pmi}, 40
\item {\ptt disp\_hypotheses}, 29
\indexspace
\item {\ptt empty\_rules}, 41
\item {\ptt END\_STACK}, 14, 42
\item {\ptt END\_STACK\_TAC}, 42
\item {\ptt equiv\_tm}, 44
\item {\ptt ESTABLISH}, 13, 44
\item {\ptt establish}, 45
\item {\ptt EXISTS\_PMI}, 46
\indexspace
\item {\ptt FILTER\_ASM\_REWRITE\_WIN}, 46
\item {\ptt filter\_asm\_rewrite\_win}, 47
\item {\ptt FILTER\_ONCE\_ASM\_REWRITE\_WIN}, 47
\item {\ptt filter\_once\_asm\_rewrite\_win}, 48
\item {\ptt FILTER\_PURE\_ASM\_REWRITE\_WIN}, 49
\item {\ptt filter\_pure\_asm\_rewrite\_win}, 49
\item {\ptt FILTER\_PURE\_ONCE\_ASM\_REWRITE\_WIN}, 50
\item {\ptt filter\_pure\_once\_asm\_rewrite\_win}, 50
\item {\ptt FOC\_RULE\_WIN}, 8, 52
\item {\ptt foc\_rule\_win}, 52
\item {\ptt FOCUS}, 51
\item focus, 6
\item {\ptt focus}, 51
\indexspace
\item {\ptt GEN\_OPEN\_WIN}, 53
\item {\ptt gen\_open\_win}, 54
\item {\ptt GEN\_REWRITE\_WIN}, 54
\item {\ptt gen\_rewrite\_win}, 55
\item {\ptt GET\_MAX\_HIST}, 57
\indexspace
\item {\ptt hyp\_thms}, 58
\item {\ptt hypotheses}, 57
\indexspace
\item {\ptt IMP\_PMI}, 59
\item {\ptt IMP\_PMI\_CONV}, 60
\item {\ptt IMP\_REFL}, 60
\item {\ptt IMP\_REFL\_THM}, 21, 95
\item {\ptt imp\_tm}, 60
\item {\ptt IMP\_TRANS\_THM}, 21, 95
\item {\ptt is\_pmi}, 61
\item {\ptt is\_trueimp}, 61
\indexspace
\item lemma, 10--11
\item {\ptt LEMMA\_THMS}, 11, 62
\item {\ptt lemma\_thms}, 63
\item {\ptt lemmas}, 62
\item {\ptt load\_window}, 6, 63
\indexspace
\item {\ptt MATCH\_TRANSFORM\_WIN}, 8, 63
\item {\ptt match\_transform\_win}, 64
\indexspace
\item {\ptt ONCE\_ASM\_REWRITE\_WIN}, 65
\item {\ptt once\_asm\_rewrite\_win}, 65
\item {\ptt ONCE\_REWRITE\_WIN}, 65
\item {\ptt once\_rewrite\_win}, 66
\item {\ptt OPEN\_CONTEXT}, 11, 66
\item {\ptt open\_context}, 68
\item {\ptt open\_TAC}, 16, 69
\item {\ptt OPEN\_WIN}, 8--9, 70
\item {\ptt open\_win}, 71
\item {\ptt origin}, 72
\indexspace
\item {\ptt path}, 8
\item {\ptt PMI\_DEF}, \nn{6}, 95
\item {\ptt PMI\_IMP}, 72
\item {\ptt PMI\_IMP\_CONV}, 73
\item {\ptt PMI\_REFL}, 73
\item {\ptt PMI\_REFL\_THM}, 95
\item {\ptt pmi\_tm}, 74
\item {\ptt PMI\_TRANS}, 74
\item {\ptt PMI\_TRANS\_THM}, 95
\item {\ptt PRINT\_STACK}, 7, 74
\item {\ptt PURE\_ASM\_REWRITE\_WIN}, 75
\item {\ptt pure\_asm\_rewrite\_win}, 75
\item {\ptt PURE\_ONCE\_ASM\_REWRITE\_WIN}, 76
\item {\ptt pure\_once\_asm\_rewrite\_win}, 76
\item {\ptt PURE\_ONCE\_REWRITE\_WIN}, 77
\item {\ptt pure\_once\_rewrite\_win}, 77
\item {\ptt PURE\_REWRITE\_WIN}, 8, 78
\item {\ptt pure\_rewrite\_win}, 78
\indexspace
\item {\ptt REDO}, 79
\item relation, 6
\item {\ptt relation}, 79
\item {\ptt REWRITE\_WIN}, 8, 80
\item {\ptt rewrite\_win}, 80
\item {\ptt RULE\_WIN}, 8, 81
\item {\ptt rule\_win}, 81
\indexspace
\item {\ptt SAVE\_WIN\_THM}, 82
\item {\ptt SET\_MAX\_HIST}, 83
\item {\ptt SET\_STACK}, 14, 83
\item {\ptt SMASH}, 83
\item {\ptt store\_rule}, 19, 84
\item stronger, 21
\item supposition, 12
\item {\ptt suppositions}, 85
\indexspace
\item {\ptt TACTIC\_WIN}, 8, 85
\item {\ptt tactic\_win}, 86
\item {\ptt THM\_RULE\_WIN}, 8, 86
\item {\ptt thm\_rule\_win}, 87
\item {\ptt TOP\_WIN}, 16, 88
\item {\ptt transform}, 16, 88
\item {\ptt TRANSFORM\_WIN}, 8, 89
\item {\ptt transform\_win}, 89
\item {\ptt traverse}, 90
\indexspace
\item {\ptt UNDO}, 8, 9, 90
\item {\ptt UNDO\_WIN}, 9, 91
\item {\ptt used\_conjectures}, 91
\item {\ptt used\_hypotheses}, 92
\indexspace
\item {\ptt WIN\_THM}, 7, 93
\item {\ptt win\_thm}, 93
\item {\ptt window\_rule}, 19
\item {\ptt window\_version}, 92
\end{theindex}
|
