equal
deleted
inserted
replaced
71 "find_consts" |
71 "find_consts" |
72 "find_theorems" |
72 "find_theorems" |
73 "fix" |
73 "fix" |
74 "from" |
74 "from" |
75 "full_prf" |
75 "full_prf" |
76 "global" |
|
77 "guess" |
76 "guess" |
78 "have" |
77 "have" |
79 "header" |
78 "header" |
80 "help" |
79 "help" |
81 "hence" |
80 "hence" |
95 "kill_thy" |
94 "kill_thy" |
96 "lemma" |
95 "lemma" |
97 "lemmas" |
96 "lemmas" |
98 "let" |
97 "let" |
99 "linear_undo" |
98 "linear_undo" |
100 "local" |
|
101 "local_setup" |
99 "local_setup" |
102 "locale" |
100 "locale" |
103 "method_setup" |
101 "method_setup" |
104 "moreover" |
102 "moreover" |
105 "next" |
103 "next" |
367 "definition" |
365 "definition" |
368 "defs" |
366 "defs" |
369 "extract" |
367 "extract" |
370 "extract_type" |
368 "extract_type" |
371 "finalconsts" |
369 "finalconsts" |
372 "global" |
|
373 "hide_class" |
370 "hide_class" |
374 "hide_const" |
371 "hide_const" |
375 "hide_fact" |
372 "hide_fact" |
376 "hide_type" |
373 "hide_type" |
377 "inductive" |
374 "inductive" |
378 "instantiation" |
375 "instantiation" |
379 "judgment" |
376 "judgment" |
380 "lemmas" |
377 "lemmas" |
381 "local" |
|
382 "local_setup" |
378 "local_setup" |
383 "locale" |
379 "locale" |
384 "method_setup" |
380 "method_setup" |
385 "no_notation" |
381 "no_notation" |
386 "no_syntax" |
382 "no_syntax" |