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
|
\indexentry{<==@{{\ptt <==} (backward implication)}|see{{\ptt PMI\_DEF}}}{2}
\indexentry{PMI\_DEF@{\ptt PMI\_DEF}|nn}{6}
\indexentry{load\_window@{\ptt load\_window}}{6}
\indexentry{focus}{6}
\indexentry{assumptions}{6}
\indexentry{relation}{6}
\indexentry{"!@{{\ptt "!} (assumption prefix)}}{6}
\indexentry{BEGIN\_STACK@{\ptt BEGIN\_STACK}|(}{6}
\indexentry{BEGIN\_STACK@{\ptt BEGIN\_STACK}|)}{7}
\indexentry{PRINT\_STACK@{\ptt PRINT\_STACK}|(}{7}
\indexentry{PRINT\_STACK@{\ptt PRINT\_STACK}|)}{7}
\indexentry{WIN\_THM@{\ptt WIN\_THM}|(}{7}
\indexentry{WIN\_THM@{\ptt WIN\_THM}|)}{7}
\indexentry{TRANSFORM\_WIN@{\ptt TRANSFORM\_WIN}}{8}
\indexentry{MATCH\_TRANSFORM\_WIN@{\ptt MATCH\_TRANSFORM\_WIN}}{8}
\indexentry{REWRITE\_WIN@{\ptt REWRITE\_WIN}}{8}
\indexentry{PURE\_REWRITE\_WIN@{\ptt PURE\_REWRITE\_WIN}}{8}
\indexentry{CONVERT\_WIN@{\ptt CONVERT\_WIN}}{8}
\indexentry{RULE\_WIN@{\ptt RULE\_WIN}}{8}
\indexentry{THM\_RULE\_WIN@{\ptt THM\_RULE\_WIN}}{8}
\indexentry{FOC\_RULE\_WIN@{\ptt FOC\_RULE\_WIN}}{8}
\indexentry{TACTIC\_WIN@{\ptt TACTIC\_WIN}}{8}
\indexentry{UNDO@{\ptt UNDO}}{8}
\indexentry{OPEN\_WIN@{\ptt OPEN\_WIN}|(}{8}
\indexentry{path@{\ptt path}}{8}
\indexentry{CLOSE\_WIN@{\ptt CLOSE\_WIN}|(}{9}
\indexentry{CLOSE\_WIN@{\ptt CLOSE\_WIN}|)}{9}
\indexentry{UNDO\_WIN@{\ptt UNDO\_WIN}}{9}
\indexentry{UNDO@{\ptt UNDO}}{9}
\indexentry{OPEN\_WIN@{\ptt OPEN\_WIN}|)}{9}
\indexentry{lemma|(}{10}
\indexentry{"|@{{\ptt "|} (lemma prefix)}}{10}
\indexentry{ADD\_THEOREM@{\ptt ADD\_THEOREM}}{10}
\indexentry{LEMMA\_THMS@{\ptt LEMMA\_THMS}}{11}
\indexentry{lemma|)}{11}
\indexentry{OPEN\_CONTEXT@{\ptt OPEN\_CONTEXT}}{11}
\indexentry{supposition}{12}
\indexentry{ADD\_SUPPOSE@{\ptt ADD\_SUPPOSE}}{12}
\indexentry{CONJECTURE@{\ptt CONJECTURE}}{12}
\indexentry{applicable}{12}
\indexentry{conjectures}{12}
\indexentry{?@{{\ptt ?} (conjecture prefix)}}{12}
\indexentry{conjectures!used}{12}
\indexentry{\$@{{\ptt \$} (used conjecture prefix)}}{12}
\indexentry{conjectures!bad}{12}
\indexentry{"@@{{\ptt "@} (bad conjecture prefix)}}{12}
\indexentry{BAD\_CONJECTURES@{\ptt BAD\_CONJECTURES}}{13}
\indexentry{ESTABLISH@{\ptt ESTABLISH}}{13}
\indexentry{BEGIN\_STACK@{\ptt BEGIN\_STACK}}{14}
\indexentry{BEGIN\_STACK@{\ptt BEGIN\_STACK}}{14}
\indexentry{SET\_STACK@{\ptt SET\_STACK}}{14}
\indexentry{SET\_STACK@{\ptt SET\_STACK}}{14}
\indexentry{END\_STACK@{\ptt END\_STACK}}{14}
\indexentry{END\_STACK@{\ptt END\_STACK}}{14}
\indexentry{CURRENT\_NAME@{\ptt CURRENT\_NAME}}{14}
\indexentry{ALL\_STACKS@{\ptt ALL\_STACKS}}{14}
\indexentry{CB@{\ptt CB}}{16}
\indexentry{transform@{\ptt transform}}{16}
\indexentry{TOP\_WIN@{\ptt TOP\_WIN}}{16}
\indexentry{APPLY\_TRANSFORM@{\ptt APPLY\_TRANSFORM}}{16}
\indexentry{BEGIN\_STACK\_TAC@{\ptt BEGIN\_STACK\_TAC}}{16}
\indexentry{CLOSE\_STACK\_TAC@{\ptt CLOSE\_STACK\_TAC}}{16}
\indexentry{open\_TAC@{\ptt open\_TAC}}{16}
\indexentry{store\_rule@{\ptt store\_rule}|(}{19}
\indexentry{store\_rule@{\ptt store\_rule}|)}{19}
\indexentry{window\_rule@{\ptt window\_rule}}{19}
\indexentry{add\_relation@{\ptt add\_relation}|(}{20}
\indexentry{IMP\_REFL\_THM@{\ptt IMP\_REFL\_THM}|(}{21}
\indexentry{IMP\_TRANS\_THM@{\ptt IMP\_TRANS\_THM}|(}{21}
\indexentry{IMP\_TRANS\_THM@{\ptt IMP\_TRANS\_THM}|)}{21}
\indexentry{IMP\_REFL\_THM@{\ptt IMP\_REFL\_THM}|)}{21}
\indexentry{add\_relation@{\ptt add\_relation}|)}{21}
\indexentry{stronger}{21}
\indexentry{add\_weak@{\ptt add\_weak}|(}{21}
\indexentry{add\_weak@{\ptt add\_weak}|)}{21}
\indexentry{add\_relation@{\ptt add\_relation}}{25}
\indexentry{ADD\_SUPPOSE@{\ptt ADD\_SUPPOSE}}{26}
\indexentry{add\_suppose@{\ptt add\_suppose}}{26}
\indexentry{ADD\_THEOREM@{\ptt ADD\_THEOREM}}{27}
\indexentry{add\_theorem@{\ptt add\_theorem}}{27}
\indexentry{add\_weak@{\ptt add\_weak}}{28}
\indexentry{disp\_hypotheses@{\ptt disp\_hypotheses}}{29}
\indexentry{ALL\_STACKS@{\ptt ALL\_STACKS}}{30}
\indexentry{APPLY\_TRANSFORM@{\ptt APPLY\_TRANSFORM}}{30}
\indexentry{ASM\_REWRITE\_WIN@{\ptt ASM\_REWRITE\_WIN}}{30}
\indexentry{asm\_rewrite\_win@{\ptt asm\_rewrite\_win}}{31}
\indexentry{BAD\_CONJECTURES@{\ptt BAD\_CONJECTURES}}{31}
\indexentry{BEGIN\_STACK@{\ptt BEGIN\_STACK}}{32}
\indexentry{BEGIN\_STACK\_TAC@{\ptt BEGIN\_STACK\_TAC}}{33}
\indexentry{bound@{\ptt bound}}{34}
\indexentry{CLOSE\_WIN@{\ptt CLOSE\_WIN}}{35}
\indexentry{CONJECTURE@{\ptt CONJECTURE}}{36}
\indexentry{conjecture@{\ptt conjecture}}{37}
\indexentry{conjectures@{\ptt conjectures}}{37}
\indexentry{context@{\ptt context}}{38}
\indexentry{CONVERT\_WIN@{\ptt CONVERT\_WIN}}{38}
\indexentry{convert\_win@{\ptt convert\_win}}{39}
\indexentry{create\_win@{\ptt create\_win}}{39}
\indexentry{CURRENT\_NAME@{\ptt CURRENT\_NAME}}{40}
\indexentry{dest\_pmi@{\ptt dest\_pmi}}{40}
\indexentry{all\_hypotheses@{\ptt all\_hypotheses}}{40}
\indexentry{empty\_rules@{\ptt empty\_rules}}{41}
\indexentry{END\_STACK@{\ptt END\_STACK}}{42}
\indexentry{END\_STACK\_TAC@{\ptt END\_STACK\_TAC}}{42}
\indexentry{equiv\_tm@{\ptt equiv\_tm}}{44}
\indexentry{ESTABLISH@{\ptt ESTABLISH}}{44}
\indexentry{establish@{\ptt establish}}{45}
\indexentry{EXISTS\_PMI@{\ptt EXISTS\_PMI}}{46}
\indexentry{FILTER\_ASM\_REWRITE\_WIN@{\ptt FILTER\_ASM\_REWRITE\_WIN}}{46}
\indexentry{filter\_asm\_rewrite\_win@{\ptt filter\_asm\_rewrite\_win}}{47}
\indexentry{FILTER\_ONCE\_ASM\_REWRITE\_WIN@{\ptt FILTER\_ONCE\_ASM\_REWRITE\_WIN}}{47}
\indexentry{filter\_once\_asm\_rewrite\_win@{\ptt filter\_once\_asm\_rewrite\_win}}{48}
\indexentry{FILTER\_PURE\_ASM\_REWRITE\_WIN@{\ptt FILTER\_PURE\_ASM\_REWRITE\_WIN}}{49}
\indexentry{filter\_pure\_asm\_rewrite\_win@{\ptt filter\_pure\_asm\_rewrite\_win}}{49}
\indexentry{FILTER\_PURE\_ONCE\_ASM\_REWRITE\_WIN@{\ptt FILTER\_PURE\_ONCE\_ASM\_REWRITE\_WIN}}{50}
\indexentry{filter\_pure\_once\_asm\_rewrite\_win@{\ptt filter\_pure\_once\_asm\_rewrite\_win}}{50}
\indexentry{FOCUS@{\ptt FOCUS}}{51}
\indexentry{focus@{\ptt focus}}{51}
\indexentry{FOC\_RULE\_WIN@{\ptt FOC\_RULE\_WIN}}{52}
\indexentry{foc\_rule\_win@{\ptt foc\_rule\_win}}{52}
\indexentry{GEN\_OPEN\_WIN@{\ptt GEN\_OPEN\_WIN}}{53}
\indexentry{gen\_open\_win@{\ptt gen\_open\_win}}{54}
\indexentry{GEN\_REWRITE\_WIN@{\ptt GEN\_REWRITE\_WIN}}{54}
\indexentry{gen\_rewrite\_win@{\ptt gen\_rewrite\_win}}{55}
\indexentry{GET\_MAX\_HIST@{\ptt GET\_MAX\_HIST}}{57}
\indexentry{hypotheses@{\ptt hypotheses}}{57}
\indexentry{hyp\_thms@{\ptt hyp\_thms}}{58}
\indexentry{IMP\_PMI@{\ptt IMP\_PMI}}{59}
\indexentry{IMP\_PMI\_CONV@{\ptt IMP\_PMI\_CONV}}{60}
\indexentry{IMP\_REFL@{\ptt IMP\_REFL}}{60}
\indexentry{imp\_tm@{\ptt imp\_tm}}{60}
\indexentry{is\_pmi@{\ptt is\_pmi}}{61}
\indexentry{is\_trueimp@{\ptt is\_trueimp}}{61}
\indexentry{lemmas@{\ptt lemmas}}{62}
\indexentry{LEMMA\_THMS@{\ptt LEMMA\_THMS}}{62}
\indexentry{lemma\_thms@{\ptt lemma\_thms}}{63}
\indexentry{load\_window@{\ptt load\_window}}{63}
\indexentry{MATCH\_TRANSFORM\_WIN@{\ptt MATCH\_TRANSFORM\_WIN}}{63}
\indexentry{match\_transform\_win@{\ptt match\_transform\_win}}{64}
\indexentry{ONCE\_ASM\_REWRITE\_WIN@{\ptt ONCE\_ASM\_REWRITE\_WIN}}{65}
\indexentry{once\_asm\_rewrite\_win@{\ptt once\_asm\_rewrite\_win}}{65}
\indexentry{ONCE\_REWRITE\_WIN@{\ptt ONCE\_REWRITE\_WIN}}{65}
\indexentry{once\_rewrite\_win@{\ptt once\_rewrite\_win}}{66}
\indexentry{OPEN\_CONTEXT@{\ptt OPEN\_CONTEXT}}{66}
\indexentry{open\_context@{\ptt open\_context}}{68}
\indexentry{open\_TAC@{\ptt open\_TAC}}{69}
\indexentry{OPEN\_WIN@{\ptt OPEN\_WIN}}{70}
\indexentry{open\_win@{\ptt open\_win}}{71}
\indexentry{origin@{\ptt origin}}{72}
\indexentry{PMI\_IMP@{\ptt PMI\_IMP}}{72}
\indexentry{PMI\_IMP\_CONV@{\ptt PMI\_IMP\_CONV}}{73}
\indexentry{PMI\_REFL@{\ptt PMI\_REFL}}{73}
\indexentry{pmi\_tm@{\ptt pmi\_tm}}{74}
\indexentry{PMI\_TRANS@{\ptt PMI\_TRANS}}{74}
\indexentry{PRINT\_STACK@{\ptt PRINT\_STACK}}{74}
\indexentry{PURE\_ASM\_REWRITE\_WIN@{\ptt PURE\_ASM\_REWRITE\_WIN}}{75}
\indexentry{pure\_asm\_rewrite\_win@{\ptt pure\_asm\_rewrite\_win}}{75}
\indexentry{PURE\_ONCE\_ASM\_REWRITE\_WIN@{\ptt PURE\_ONCE\_ASM\_REWRITE\_WIN}}{76}
\indexentry{pure\_once\_asm\_rewrite\_win@{\ptt pure\_once\_asm\_rewrite\_win}}{76}
\indexentry{PURE\_ONCE\_REWRITE\_WIN@{\ptt PURE\_ONCE\_REWRITE\_WIN}}{77}
\indexentry{pure\_once\_rewrite\_win@{\ptt pure\_once\_rewrite\_win}}{77}
\indexentry{PURE\_REWRITE\_WIN@{\ptt PURE\_REWRITE\_WIN}}{78}
\indexentry{pure\_rewrite\_win@{\ptt pure\_rewrite\_win}}{78}
\indexentry{REDO@{\ptt REDO}}{79}
\indexentry{relation@{\ptt relation}}{79}
\indexentry{REWRITE\_WIN@{\ptt REWRITE\_WIN}}{80}
\indexentry{rewrite\_win@{\ptt rewrite\_win}}{80}
\indexentry{RULE\_WIN@{\ptt RULE\_WIN}}{81}
\indexentry{rule\_win@{\ptt rule\_win}}{81}
\indexentry{SAVE\_WIN\_THM@{\ptt SAVE\_WIN\_THM}}{82}
\indexentry{SET\_MAX\_HIST@{\ptt SET\_MAX\_HIST}}{83}
\indexentry{SET\_STACK@{\ptt SET\_STACK}}{83}
\indexentry{SMASH@{\ptt SMASH}}{83}
\indexentry{store\_rule@{\ptt store\_rule}}{84}
\indexentry{suppositions@{\ptt suppositions}}{85}
\indexentry{TACTIC\_WIN@{\ptt TACTIC\_WIN}}{85}
\indexentry{tactic\_win@{\ptt tactic\_win}}{86}
\indexentry{THM\_RULE\_WIN@{\ptt THM\_RULE\_WIN}}{86}
\indexentry{thm\_rule\_win@{\ptt thm\_rule\_win}}{87}
\indexentry{TOP\_WIN@{\ptt TOP\_WIN}}{88}
\indexentry{transform@{\ptt transform}}{88}
\indexentry{TRANSFORM\_WIN@{\ptt TRANSFORM\_WIN}}{89}
\indexentry{transform\_win@{\ptt transform\_win}}{89}
\indexentry{traverse@{\ptt traverse}}{90}
\indexentry{UNDO@{\ptt UNDO}}{90}
\indexentry{UNDO\_WIN@{\ptt UNDO\_WIN}}{91}
\indexentry{used\_conjectures@{\ptt used\_conjectures}}{91}
\indexentry{used\_hypotheses@{\ptt used\_hypotheses}}{92}
\indexentry{window\_version@{\ptt window\_version}}{92}
\indexentry{WIN\_THM@{\ptt WIN\_THM}}{93}
\indexentry{win\_thm@{\ptt win\_thm}}{93}
\indexentry{PMI\_DEF@{\ptt PMI\_DEF}}{95}
\indexentry{IMP\_REFL\_THM@{\ptt IMP\_REFL\_THM}}{95}
\indexentry{IMP\_TRANS\_THM@{\ptt IMP\_TRANS\_THM}}{95}
\indexentry{PMI\_DEF@{\ptt PMI\_DEF}}{95}
\indexentry{PMI\_REFL\_THM@{\ptt PMI\_REFL\_THM}}{95}
\indexentry{PMI\_TRANS\_THM@{\ptt PMI\_TRANS\_THM}}{95}
|
