| changeset 24249 | 1f60b45c5f97 |
| parent 24111 | 20e74aa5f56b |
| child 24343 | acc0f7aac619 |
| 24248:d276e4b53d6b | 24249:1f60b45c5f97 |
|---|---|
108 "moreover" |
108 "moreover" |
109 "next" |
109 "next" |
110 "no_syntax" |
110 "no_syntax" |
111 "no_translations" |
111 "no_translations" |
112 "nonterminals" |
112 "nonterminals" |
113 "normal_form" |
|
114 "notation" |
113 "notation" |
115 "note" |
114 "note" |
116 "obtain" |
115 "obtain" |
117 "oops" |
116 "oops" |
118 "oracle" |
117 "oracle" |
200 "types_code" |
199 "types_code" |
201 "ultimately" |
200 "ultimately" |
202 "undo" |
201 "undo" |
203 "undos_proof" |
202 "undos_proof" |
204 "unfolding" |
203 "unfolding" |
205 "update_thy" |
|
206 "use" |
204 "use" |
207 "use_thy" |
205 "use_thy" |
208 "using" |
206 "using" |
209 "value" |
207 "value" |
210 "welcome" |
208 "welcome" |
239 "infix" |
237 "infix" |
240 "infixl" |
238 "infixl" |
241 "infixr" |
239 "infixr" |
242 "intros" |
240 "intros" |
243 "is" |
241 "is" |
242 "module_name" |
|
244 "monos" |
243 "monos" |
245 "notes" |
244 "notes" |
246 "obtains" |
245 "obtains" |
247 "open" |
246 "open" |
248 "output" |
247 "output" |
249 "overloaded" |
248 "overloaded" |
250 "recursor_eqns" |
249 "recursor_eqns" |
251 "shows" |
250 "shows" |
252 "structure" |
251 "structure" |
253 "to" |
|
254 "type_elims" |
252 "type_elims" |
255 "type_intros" |
253 "type_intros" |
256 "unchecked" |
254 "unchecked" |
257 "uses" |
255 "uses" |
258 "where")) |
256 "where")) |
288 "find_theorems" |
286 "find_theorems" |
289 "full_prf" |
287 "full_prf" |
290 "header" |
288 "header" |
291 "help" |
289 "help" |
292 "kill_thy" |
290 "kill_thy" |
293 "normal_form" |
|
294 "pr" |
291 "pr" |
295 "pretty_setmargin" |
292 "pretty_setmargin" |
296 "prf" |
293 "prf" |
297 "print_abbrevs" |
294 "print_abbrevs" |
298 "print_antiquotations" |
295 "print_antiquotations" |
330 "thy_deps" |
327 "thy_deps" |
331 "touch_all_thys" |
328 "touch_all_thys" |
332 "touch_child_thys" |
329 "touch_child_thys" |
333 "touch_thy" |
330 "touch_thy" |
334 "typ" |
331 "typ" |
335 "update_thy" |
|
336 "use" |
332 "use" |
337 "use_thy" |
333 "use_thy" |
338 "value" |
334 "value" |
339 "welcome")) |
335 "welcome")) |
340 |
336 |