src/Pure/Pure.thy
changeset 51270 17d30843fc3b
parent 51224 c3e99efacb67
child 51274 cfc83ad52571
equal deleted inserted replaced
51269:54725c4acdd0 51270:17d30843fc3b
    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