equal
deleted
inserted
replaced
73 and "proof" :: prf_block % "proof" |
73 and "proof" :: prf_block % "proof" |
74 and "also" "moreover" :: prf_decl % "proof" |
74 and "also" "moreover" :: prf_decl % "proof" |
75 and "finally" "ultimately" :: prf_chain % "proof" |
75 and "finally" "ultimately" :: prf_chain % "proof" |
76 and "back" :: prf_script % "proof" |
76 and "back" :: prf_script % "proof" |
77 and "Isabelle.command" :: control |
77 and "Isabelle.command" :: control |
78 and "pretty_setmargin" "help" "print_commands" "print_configs" |
78 and "help" "print_commands" "print_configs" |
79 "print_context" "print_theory" "print_syntax" "print_abbrevs" |
79 "print_context" "print_theory" "print_syntax" "print_abbrevs" |
80 "print_theorems" "print_locales" "print_classes" "print_locale" |
80 "print_theorems" "print_locales" "print_classes" "print_locale" |
81 "print_interps" "print_dependencies" "print_attributes" |
81 "print_interps" "print_dependencies" "print_attributes" |
82 "print_simpset" "print_rules" "print_trans_rules" "print_methods" |
82 "print_simpset" "print_rules" "print_trans_rules" "print_methods" |
83 "print_antiquotations" "thy_deps" "locale_deps" "class_deps" "thm_deps" |
83 "print_antiquotations" "thy_deps" "locale_deps" "class_deps" "thm_deps" |
86 :: diag |
86 :: diag |
87 and "cd" :: control |
87 and "cd" :: control |
88 and "pwd" :: diag |
88 and "pwd" :: diag |
89 and "use_thy" "remove_thy" "kill_thy" :: control |
89 and "use_thy" "remove_thy" "kill_thy" :: control |
90 and "display_drafts" "print_drafts" "pr" :: diag |
90 and "display_drafts" "print_drafts" "pr" :: diag |
91 and "disable_pr" "enable_pr" "commit" "quit" "exit" :: control |
91 and "pretty_setmargin" "disable_pr" "enable_pr" "commit" "quit" "exit" :: control |
92 and "welcome" :: diag |
92 and "welcome" :: diag |
93 and "init_toplevel" "linear_undo" "undo" "undos_proof" "cannot_undo" "kill" :: control |
93 and "init_toplevel" "linear_undo" "undo" "undos_proof" "cannot_undo" "kill" :: control |
94 and "end" :: thy_end % "theory" |
94 and "end" :: thy_end % "theory" |
95 and "realizers" "realizability" "extract_type" "extract" :: thy_decl |
95 and "realizers" "realizability" "extract_type" "extract" :: thy_decl |
96 and "find_theorems" "find_consts" :: diag |
96 and "find_theorems" "find_consts" :: diag |