author  wenzelm 
Fri, 10 Jun 2016 22:47:25 +0200  
changeset 63282  7c509ddf29a5 
parent 63273  302daf918966 
child 63285  e9c777bfd78c 
permissions  rwrr 
48929
05d4e5f660ae
entity markup for theory Pure, to enable hyperlinks etc.;
wenzelm
parents:
48891
diff
changeset

1 
(* Title: Pure/Pure.thy 
05d4e5f660ae
entity markup for theory Pure, to enable hyperlinks etc.;
wenzelm
parents:
48891
diff
changeset

2 
Author: Makarius 
05d4e5f660ae
entity markup for theory Pure, to enable hyperlinks etc.;
wenzelm
parents:
48891
diff
changeset

3 

62944
3ee643c5ed00
more standard session build process, including browser_info;
wenzelm
parents:
62913
diff
changeset

4 
The Pure theory, with definitions of Isar commands and some lemmas. 
48929
05d4e5f660ae
entity markup for theory Pure, to enable hyperlinks etc.;
wenzelm
parents:
48891
diff
changeset

5 
*) 
05d4e5f660ae
entity markup for theory Pure, to enable hyperlinks etc.;
wenzelm
parents:
48891
diff
changeset

6 

48638  7 
theory Pure 
62859  8 
keywords 
61579  9 
"!!" "!" "+" "" ":" ";" "<" "<=" "=" "=>" "?" "[" "\<comment>" "\<equiv>" 
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58918
diff
changeset

10 
"\<leftharpoondown>" "\<rightharpoonup>" "\<rightleftharpoons>" 
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58918
diff
changeset

11 
"\<subseteq>" "]" "assumes" "attach" "binder" "constrains" 
62913  12 
"defines" "rewrites" "fixes" "for" "if" "in" "includes" "infix" 
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58918
diff
changeset

13 
"infixl" "infixr" "is" "notes" "obtains" "open" "output" 
61566
c3d6e570ccef
Keyword 'rewrites' identifies rewrite morphisms.
ballarin
parents:
61338
diff
changeset

14 
"overloaded" "pervasive" "premises" "private" "qualified" "rewrites" 
c3d6e570ccef
Keyword 'rewrites' identifies rewrite morphisms.
ballarin
parents:
61338
diff
changeset

15 
"shows" "structure" "unchecked" "where" "when" "" 
58999
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58928
diff
changeset

16 
and "text" "txt" :: document_body 
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58928
diff
changeset

17 
and "text_raw" :: document_raw 
57506  18 
and "default_sort" :: thy_decl == "" 
19 
and "typedecl" "type_synonym" "nonterminal" "judgment" 

62169  20 
"consts" "syntax" "no_syntax" "translations" "no_translations" 
55385
169e12bbf9a3
discontinued axiomatic 'classes', 'classrel', 'arities';
wenzelm
parents:
55152
diff
changeset

21 
"definition" "abbreviation" "type_notation" "no_type_notation" "notation" 
61337  22 
"no_notation" "axiomatization" "lemmas" "declare" 
48641
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

23 
"hide_class" "hide_type" "hide_const" "hide_fact" :: thy_decl 
62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

24 
and "ML_file" "ML_file_debug" "ML_file_no_debug" :: thy_load % "ML" 
60957
574254152856
support for ML files with/without debugger information;
wenzelm
parents:
60749
diff
changeset

25 
and "SML_file" "SML_file_debug" "SML_file_no_debug" :: thy_load % "ML" 
56618
874bdedb2313
added command 'SML_export' and 'SML_import' for exchange of toplevel bindings;
wenzelm
parents:
56275
diff
changeset

26 
and "SML_import" "SML_export" :: thy_decl % "ML" 
48641
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

27 
and "ML_prf" :: prf_decl % "proof" (* FIXME % "ML" ?? *) 
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

28 
and "ML_val" "ML_command" :: diag % "ML" 
55762
27a45aec67a0
suppress completion of obscure keyword, avoid confusion with plain "simp";
wenzelm
parents:
55516
diff
changeset

29 
and "simproc_setup" :: thy_decl % "ML" == "" 
48641
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

30 
and "setup" "local_setup" "attribute_setup" "method_setup" 
55762
27a45aec67a0
suppress completion of obscure keyword, avoid confusion with plain "simp";
wenzelm
parents:
55516
diff
changeset

31 
"declaration" "syntax_declaration" 
48641
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

32 
"parse_ast_translation" "parse_translation" "print_translation" 
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

33 
"typed_print_translation" "print_ast_translation" "oracle" :: thy_decl % "ML" 
63273  34 
and "bundle" :: thy_decl_block 
63282  35 
and "unbundle" :: thy_decl 
48641
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

36 
and "include" "including" :: prf_decl 
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

37 
and "print_bundles" :: diag 
59901  38 
and "context" "locale" "experiment" :: thy_decl_block 
51224
c3e99efacb67
back to nonschematic 'sublocale' and 'interpretation' (despite df8fc0567a3d) for more potential parallelism;
wenzelm
parents:
50603
diff
changeset

39 
and "interpret" :: prf_goal % "proof" 
61890
f6ded81f5690
abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents:
61853
diff
changeset

40 
and "interpretation" "global_interpretation" "sublocale" :: thy_goal 
58800
bfed1c26caed
explicit keyword category for commands that may start a block;
wenzelm
parents:
58660
diff
changeset

41 
and "class" :: thy_decl_block 
48641
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

42 
and "subclass" :: thy_goal 
58800
bfed1c26caed
explicit keyword category for commands that may start a block;
wenzelm
parents:
58660
diff
changeset

43 
and "instantiation" :: thy_decl_block 
48641
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

44 
and "instance" :: thy_goal 
58800
bfed1c26caed
explicit keyword category for commands that may start a block;
wenzelm
parents:
58660
diff
changeset

45 
and "overloading" :: thy_decl_block 
48641
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

46 
and "code_datatype" :: thy_decl 
61338  47 
and "theorem" "lemma" "corollary" "proposition" :: thy_goal 
61337  48 
and "schematic_goal" :: thy_goal 
58800
bfed1c26caed
explicit keyword category for commands that may start a block;
wenzelm
parents:
58660
diff
changeset

49 
and "notepad" :: thy_decl_block 
50128
599c935aac82
alternative completion for outer syntax keywords;
wenzelm
parents:
49569
diff
changeset

50 
and "have" :: prf_goal % "proof" 
599c935aac82
alternative completion for outer syntax keywords;
wenzelm
parents:
49569
diff
changeset

51 
and "hence" :: prf_goal % "proof" == "then have" 
599c935aac82
alternative completion for outer syntax keywords;
wenzelm
parents:
49569
diff
changeset

52 
and "show" :: prf_asm_goal % "proof" 
599c935aac82
alternative completion for outer syntax keywords;
wenzelm
parents:
49569
diff
changeset

53 
and "thus" :: prf_asm_goal % "proof" == "then show" 
48641
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

54 
and "then" "from" "with" :: prf_chain % "proof" 
60371  55 
and "note" :: prf_decl % "proof" 
56 
and "supply" :: prf_script % "proof" 

57 
and "using" "unfolding" :: prf_decl % "proof" 

63039  58 
and "fix" "assume" "presume" "define" "def" :: prf_asm % "proof" 
60448  59 
and "consider" :: prf_goal % "proof" 
53371
47b23c582127
more explicit indication of 'guess' as improper Isar (aka "script") element;
wenzelm
parents:
52549
diff
changeset

60 
and "obtain" :: prf_asm_goal % "proof" 
60624  61 
and "guess" :: prf_script_asm_goal % "proof" 
48641
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

62 
and "let" "write" :: prf_decl % "proof" 
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

63 
and "case" :: prf_asm % "proof" 
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

64 
and "{" :: prf_open % "proof" 
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

65 
and "}" :: prf_close % "proof" 
60694
b3fa4a8cdb5f
clarified text folds: proof ... qed counts as extra block;
wenzelm
parents:
60624
diff
changeset

66 
and "next" :: next_block % "proof" 
48641
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

67 
and "qed" :: qed_block % "proof" 
62312
5e5a881ebc12
command '\<proof>' is an alias for 'sorry', with different typesetting;
wenzelm
parents:
62169
diff
changeset

68 
and "by" ".." "." "sorry" "\<proof>" :: "qed" % "proof" 
53571
e58ca0311c0f
more explicit indication of 'done' as proof script element;
wenzelm
parents:
53371
diff
changeset

69 
and "done" :: "qed_script" % "proof" 
48641
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

70 
and "oops" :: qed_global % "proof" 
50128
599c935aac82
alternative completion for outer syntax keywords;
wenzelm
parents:
49569
diff
changeset

71 
and "defer" "prefer" "apply" :: prf_script % "proof" 
599c935aac82
alternative completion for outer syntax keywords;
wenzelm
parents:
49569
diff
changeset

72 
and "apply_end" :: prf_script % "proof" == "" 
60624  73 
and "subgoal" :: prf_script_goal % "proof" 
48641
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

74 
and "proof" :: prf_block % "proof" 
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

75 
and "also" "moreover" :: prf_decl % "proof" 
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

76 
and "finally" "ultimately" :: prf_chain % "proof" 
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

77 
and "back" :: prf_script % "proof" 
61252  78 
and "help" "print_commands" "print_options" "print_context" "print_theory" 
79 
"print_definitions" "print_syntax" "print_abbrevs" "print_defn_rules" 

48641
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

80 
"print_theorems" "print_locales" "print_classes" "print_locale" 
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

81 
"print_interps" "print_dependencies" "print_attributes" 
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

82 
"print_simpset" "print_rules" "print_trans_rules" "print_methods" 
56069
451d5b73f8cf
simplified programming interface to define ML antiquotations  NB: the transformed context ignores updates of the context parser;
wenzelm
parents:
55762
diff
changeset

83 
"print_antiquotations" "print_ML_antiquotations" "thy_deps" 
58845  84 
"locale_deps" "class_deps" "thm_deps" "print_term_bindings" 
57415
e721124f1b1e
command 'print_term_bindings' supersedes 'print_binds';
wenzelm
parents:
56864
diff
changeset

85 
"print_facts" "print_cases" "print_statement" "thm" "prf" "full_prf" 
e721124f1b1e
command 'print_term_bindings' supersedes 'print_binds';
wenzelm
parents:
56864
diff
changeset

86 
"prop" "term" "typ" "print_codesetup" "unused_thms" :: diag 
58845  87 
and "display_drafts" "print_state" :: diag 
48646
91281e9472d8
more official command specifications, including source position;
wenzelm
parents:
48641
diff
changeset

88 
and "welcome" :: diag 
48641
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

89 
and "end" :: thy_end % "theory" 
56797  90 
and "realizers" :: thy_decl == "" 
91 
and "realizability" :: thy_decl == "" 

92 
and "extract_type" "extract" :: thy_decl 

48646
91281e9472d8
more official command specifications, including source position;
wenzelm
parents:
48641
diff
changeset

93 
and "find_theorems" "find_consts" :: diag 
57886
7cae177c9084
support for named collections of theorems in canonical order;
wenzelm
parents:
57506
diff
changeset

94 
and "named_theorems" :: thy_decl 
48638  95 
begin 
15803  96 

62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

97 
section \<open>Isar commands\<close> 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

98 

62856  99 
subsection \<open>Embedded ML text\<close> 
62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

100 

62856  101 
ML \<open> 
62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

102 
local 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

103 

62902
3c0f53eae166
more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use';
wenzelm
parents:
62898
diff
changeset

104 
val semi = Scan.option @{keyword ";"}; 
3c0f53eae166
more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use';
wenzelm
parents:
62898
diff
changeset

105 

62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

106 
val _ = 
62867  107 
Outer_Syntax.command @{command_keyword ML_file} "read and evaluate Isabelle/ML file" 
62902
3c0f53eae166
more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use';
wenzelm
parents:
62898
diff
changeset

108 
(Resources.parse_files "ML_file"  semi >> ML_File.ML NONE); 
62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

109 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

110 
val _ = 
62867  111 
Outer_Syntax.command @{command_keyword ML_file_debug} 
62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

112 
"read and evaluate Isabelle/ML file (with debugger information)" 
62902
3c0f53eae166
more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use';
wenzelm
parents:
62898
diff
changeset

113 
(Resources.parse_files "ML_file_debug"  semi >> ML_File.ML (SOME true)); 
62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

114 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

115 
val _ = 
62867  116 
Outer_Syntax.command @{command_keyword ML_file_no_debug} 
62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

117 
"read and evaluate Isabelle/ML file (no debugger information)" 
62902
3c0f53eae166
more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use';
wenzelm
parents:
62898
diff
changeset

118 
(Resources.parse_files "ML_file_no_debug"  semi >> ML_File.ML (SOME false)); 
62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

119 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

120 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

121 
Outer_Syntax.command @{command_keyword SML_file} "read and evaluate Standard ML file" 
62902
3c0f53eae166
more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use';
wenzelm
parents:
62898
diff
changeset

122 
(Resources.parse_files "SML_file"  semi >> ML_File.SML NONE); 
62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

123 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

124 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

125 
Outer_Syntax.command @{command_keyword SML_file_debug} 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

126 
"read and evaluate Standard ML file (with debugger information)" 
62902
3c0f53eae166
more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use';
wenzelm
parents:
62898
diff
changeset

127 
(Resources.parse_files "SML_file_debug"  semi >> ML_File.SML (SOME true)); 
62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

128 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

129 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

130 
Outer_Syntax.command @{command_keyword SML_file_no_debug} 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

131 
"read and evaluate Standard ML file (no debugger information)" 
62902
3c0f53eae166
more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use';
wenzelm
parents:
62898
diff
changeset

132 
(Resources.parse_files "SML_file_no_debug"  semi >> ML_File.SML (SOME false)); 
62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

133 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

134 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

135 
Outer_Syntax.command @{command_keyword SML_export} "evaluate SML within Isabelle/ML environment" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

136 
(Parse.ML_source >> (fn source => 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

137 
let 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

138 
val flags: ML_Compiler.flags = 
62902
3c0f53eae166
more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use';
wenzelm
parents:
62898
diff
changeset

139 
{SML = true, exchange = true, redirect = false, verbose = true, 
3c0f53eae166
more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use';
wenzelm
parents:
62898
diff
changeset

140 
debug = NONE, writeln = writeln, warning = warning}; 
62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

141 
in 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

142 
Toplevel.theory 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

143 
(Context.theory_map (ML_Context.exec (fn () => ML_Context.eval_source flags source))) 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

144 
end)); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

145 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

146 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

147 
Outer_Syntax.command @{command_keyword SML_import} "evaluate Isabelle/ML within SML environment" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

148 
(Parse.ML_source >> (fn source => 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

149 
let 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

150 
val flags: ML_Compiler.flags = 
62902
3c0f53eae166
more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use';
wenzelm
parents:
62898
diff
changeset

151 
{SML = false, exchange = true, redirect = false, verbose = true, 
3c0f53eae166
more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use';
wenzelm
parents:
62898
diff
changeset

152 
debug = NONE, writeln = writeln, warning = warning}; 
62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

153 
in 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

154 
Toplevel.generic_theory 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

155 
(ML_Context.exec (fn () => ML_Context.eval_source flags source) #> 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

156 
Local_Theory.propagate_ml_env) 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

157 
end)); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

158 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

159 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

160 
Outer_Syntax.command @{command_keyword ML_prf} "ML text within proof" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

161 
(Parse.ML_source >> (fn source => 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

162 
Toplevel.proof (Proof.map_context (Context.proof_map 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

163 
(ML_Context.exec (fn () => 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

164 
ML_Context.eval_source (ML_Compiler.verbose true ML_Compiler.flags) source))) #> 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

165 
Proof.propagate_ml_env))); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

166 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

167 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

168 
Outer_Syntax.command @{command_keyword ML_val} "diagnostic ML text" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

169 
(Parse.ML_source >> Isar_Cmd.ml_diag true); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

170 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

171 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

172 
Outer_Syntax.command @{command_keyword ML_command} "diagnostic ML text (silent)" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

173 
(Parse.ML_source >> Isar_Cmd.ml_diag false); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

174 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

175 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

176 
Outer_Syntax.command @{command_keyword setup} "ML setup for global theory" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

177 
(Parse.ML_source >> (Toplevel.theory o Isar_Cmd.setup)); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

178 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

179 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

180 
Outer_Syntax.local_theory @{command_keyword local_setup} "ML setup for local theory" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

181 
(Parse.ML_source >> Isar_Cmd.local_setup); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

182 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

183 
val _ = 
62856  184 
Outer_Syntax.command @{command_keyword oracle} "declare oracle" 
185 
(Parse.range Parse.name  (@{keyword "="}  Parse.ML_source) >> 

186 
(fn (x, y) => Toplevel.theory (Isar_Cmd.oracle x y))); 

187 

188 
val _ = 

62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

189 
Outer_Syntax.local_theory @{command_keyword attribute_setup} "define attribute in ML" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

190 
(Parse.position Parse.name  
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

191 
Parse.!!! (@{keyword "="}  Parse.ML_source  Scan.optional Parse.text "") 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

192 
>> (fn (name, (txt, cmt)) => Attrib.attribute_setup name txt cmt)); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

193 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

194 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

195 
Outer_Syntax.local_theory @{command_keyword method_setup} "define proof method in ML" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

196 
(Parse.position Parse.name  
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

197 
Parse.!!! (@{keyword "="}  Parse.ML_source  Scan.optional Parse.text "") 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

198 
>> (fn (name, (txt, cmt)) => Method.method_setup name txt cmt)); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

199 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

200 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

201 
Outer_Syntax.local_theory @{command_keyword declaration} "generic ML declaration" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

202 
(Parse.opt_keyword "pervasive"  Parse.ML_source 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

203 
>> (fn (pervasive, txt) => Isar_Cmd.declaration {syntax = false, pervasive = pervasive} txt)); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

204 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

205 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

206 
Outer_Syntax.local_theory @{command_keyword syntax_declaration} "generic ML syntax declaration" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

207 
(Parse.opt_keyword "pervasive"  Parse.ML_source 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

208 
>> (fn (pervasive, txt) => Isar_Cmd.declaration {syntax = true, pervasive = pervasive} txt)); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

209 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

210 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

211 
Outer_Syntax.local_theory @{command_keyword simproc_setup} "define simproc in ML" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

212 
(Parse.position Parse.name  
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

213 
(@{keyword "("}  Parse.enum1 "" Parse.term  @{keyword ")"}  @{keyword "="})  
62913  214 
Parse.ML_source >> (fn ((a, b), c) => Isar_Cmd.simproc_setup a b c)); 
62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

215 

62856  216 
in end\<close> 
62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

217 

62856  218 

219 
subsection \<open>Theory commands\<close> 

220 

221 
subsubsection \<open>Sorts and types\<close> 

222 

223 
ML \<open> 

224 
local 

225 

226 
val _ = 

227 
Outer_Syntax.local_theory @{command_keyword default_sort} 

228 
"declare default sort for explicit type variables" 

229 
(Parse.sort >> (fn s => fn lthy => Local_Theory.set_defsort (Syntax.read_sort lthy s) lthy)); 

230 

231 
val _ = 

232 
Outer_Syntax.local_theory @{command_keyword typedecl} "type declaration" 

233 
(Parse.type_args  Parse.binding  Parse.opt_mixfix 

234 
>> (fn ((args, a), mx) => 

235 
Typedecl.typedecl {final = true} (a, map (rpair dummyS) args, mx) #> snd)); 

236 

237 
val _ = 

238 
Outer_Syntax.local_theory @{command_keyword type_synonym} "declare type abbreviation" 

239 
(Parse.type_args  Parse.binding  

240 
(@{keyword "="}  Parse.!!! (Parse.typ  Parse.opt_mixfix')) 

241 
>> (fn ((args, a), (rhs, mx)) => snd o Typedecl.abbrev_cmd (a, args, mx) rhs)); 

242 

243 
in end\<close> 

244 

245 

246 
subsubsection \<open>Consts\<close> 

247 

248 
ML \<open> 

249 
local 

250 

251 
val _ = 

252 
Outer_Syntax.command @{command_keyword judgment} "declare objectlogic judgment" 

253 
(Parse.const_binding >> (Toplevel.theory o Object_Logic.add_judgment_cmd)); 

254 

255 
val _ = 

256 
Outer_Syntax.command @{command_keyword consts} "declare constants" 

257 
(Scan.repeat1 Parse.const_binding >> (Toplevel.theory o Sign.add_consts_cmd)); 

258 

259 
in end\<close> 

260 

261 

262 
subsubsection \<open>Syntax and translations\<close> 

263 

264 
ML \<open> 

265 
local 

266 

267 
val _ = 

268 
Outer_Syntax.command @{command_keyword nonterminal} 

269 
"declare syntactic type constructors (grammar nonterminal symbols)" 

270 
(Parse.and_list1 Parse.binding >> (Toplevel.theory o Sign.add_nonterminals_global)); 

271 

272 
val _ = 

273 
Outer_Syntax.command @{command_keyword syntax} "add raw syntax clauses" 

274 
(Parse.syntax_mode  Scan.repeat1 Parse.const_decl 

275 
>> (Toplevel.theory o uncurry Sign.add_syntax_cmd)); 

276 

277 
val _ = 

278 
Outer_Syntax.command @{command_keyword no_syntax} "delete raw syntax clauses" 

279 
(Parse.syntax_mode  Scan.repeat1 Parse.const_decl 

280 
>> (Toplevel.theory o uncurry Sign.del_syntax_cmd)); 

281 

282 
val trans_pat = 

283 
Scan.optional 

62969  284 
(@{keyword "("}  Parse.!!! (Parse.inner_syntax Parse.name  @{keyword ")"})) "logic" 
62856  285 
 Parse.inner_syntax Parse.string; 
286 

287 
fun trans_arrow toks = 

288 
((@{keyword "\<rightharpoonup>"}  @{keyword "=>"}) >> K Syntax.Parse_Rule  

289 
(@{keyword "\<leftharpoondown>"}  @{keyword "<="}) >> K Syntax.Print_Rule  

290 
(@{keyword "\<rightleftharpoons>"}  @{keyword "=="}) >> K Syntax.Parse_Print_Rule) toks; 

291 

292 
val trans_line = 

293 
trans_pat  Parse.!!! (trans_arrow  trans_pat) 

294 
>> (fn (left, (arr, right)) => arr (left, right)); 

295 

296 
val _ = 

297 
Outer_Syntax.command @{command_keyword translations} "add syntax translation rules" 

298 
(Scan.repeat1 trans_line >> (Toplevel.theory o Isar_Cmd.translations)); 

299 

300 
val _ = 

301 
Outer_Syntax.command @{command_keyword no_translations} "delete syntax translation rules" 

302 
(Scan.repeat1 trans_line >> (Toplevel.theory o Isar_Cmd.no_translations)); 

303 

304 
in end\<close> 

305 

306 

307 
subsubsection \<open>Translation functions\<close> 

308 

309 
ML \<open> 

310 
local 

62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

311 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

312 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

313 
Outer_Syntax.command @{command_keyword parse_ast_translation} 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

314 
"install parse ast translation functions" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

315 
(Parse.ML_source >> (Toplevel.theory o Isar_Cmd.parse_ast_translation)); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

316 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

317 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

318 
Outer_Syntax.command @{command_keyword parse_translation} 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

319 
"install parse translation functions" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

320 
(Parse.ML_source >> (Toplevel.theory o Isar_Cmd.parse_translation)); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

321 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

322 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

323 
Outer_Syntax.command @{command_keyword print_translation} 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

324 
"install print translation functions" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

325 
(Parse.ML_source >> (Toplevel.theory o Isar_Cmd.print_translation)); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

326 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

327 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

328 
Outer_Syntax.command @{command_keyword typed_print_translation} 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

329 
"install typed print translation functions" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

330 
(Parse.ML_source >> (Toplevel.theory o Isar_Cmd.typed_print_translation)); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

331 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

332 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

333 
Outer_Syntax.command @{command_keyword print_ast_translation} 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

334 
"install print ast translation functions" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

335 
(Parse.ML_source >> (Toplevel.theory o Isar_Cmd.print_ast_translation)); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

336 

62856  337 
in end\<close> 
62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

338 

62856  339 

340 
subsubsection \<open>Specifications\<close> 

341 

342 
ML \<open> 

343 
local 

344 

345 
val _ = 

346 
Outer_Syntax.local_theory' @{command_keyword definition} "constant definition" 

63180  347 
(Scan.option Parse_Spec.constdecl  (Parse_Spec.opt_thm_name ":"  Parse.prop)  
348 
Parse_Spec.if_assumes  Parse.for_fixes >> (fn (((decl, spec), prems), params) => 

349 
#2 oo Specification.definition_cmd decl params prems spec)); 

62856  350 

351 
val _ = 

352 
Outer_Syntax.local_theory' @{command_keyword abbreviation} "constant abbreviation" 

63180  353 
(Parse.syntax_mode  Scan.option Parse_Spec.constdecl  Parse.prop  Parse.for_fixes 
354 
>> (fn (((mode, decl), spec), params) => Specification.abbreviation_cmd mode decl params spec)); 

62856  355 

63178  356 
val axiomatization = 
357 
Parse.and_list1 (Parse_Spec.thm_name ":"  Parse.prop)  

358 
Parse_Spec.if_assumes  Parse.for_fixes >> (fn ((a, b), c) => (c, b, a)); 

359 

62856  360 
val _ = 
361 
Outer_Syntax.command @{command_keyword axiomatization} "axiomatic constant specification" 

362 
(Scan.optional Parse.fixes []  

63178  363 
Scan.optional (Parse.where_  Parse.!!! axiomatization) ([], [], []) 
364 
>> (fn (a, (b, c, d)) => Toplevel.theory (#2 o Specification.axiomatization_cmd a b c d))); 

62856  365 

366 
in end\<close> 

367 

368 

369 
subsubsection \<open>Notation\<close> 

370 

371 
ML \<open> 

372 
local 

373 

374 
val _ = 

375 
Outer_Syntax.local_theory @{command_keyword type_notation} 

376 
"add concrete syntax for type constructors" 

377 
(Parse.syntax_mode  Parse.and_list1 (Parse.type_const  Parse.mixfix) 

378 
>> (fn (mode, args) => Specification.type_notation_cmd true mode args)); 

379 

380 
val _ = 

381 
Outer_Syntax.local_theory @{command_keyword no_type_notation} 

382 
"delete concrete syntax for type constructors" 

383 
(Parse.syntax_mode  Parse.and_list1 (Parse.type_const  Parse.mixfix) 

384 
>> (fn (mode, args) => Specification.type_notation_cmd false mode args)); 

385 

386 
val _ = 

387 
Outer_Syntax.local_theory @{command_keyword notation} 

388 
"add concrete syntax for constants / fixed variables" 

389 
(Parse.syntax_mode  Parse.and_list1 (Parse.const  Parse.mixfix) 

390 
>> (fn (mode, args) => Specification.notation_cmd true mode args)); 

62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

391 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

392 
val _ = 
62856  393 
Outer_Syntax.local_theory @{command_keyword no_notation} 
394 
"delete concrete syntax for constants / fixed variables" 

395 
(Parse.syntax_mode  Parse.and_list1 (Parse.const  Parse.mixfix) 

396 
>> (fn (mode, args) => Specification.notation_cmd false mode args)); 

397 

398 
in end\<close> 

399 

400 

401 
subsubsection \<open>Theorems\<close> 

402 

403 
ML \<open> 

404 
local 

405 

63094
056ea294c256
toplevel theorem statements support 'if'/'for' eigencontext;
wenzelm
parents:
63064
diff
changeset

406 
val long_keyword = 
056ea294c256
toplevel theorem statements support 'if'/'for' eigencontext;
wenzelm
parents:
63064
diff
changeset

407 
Parse_Spec.includes >> K ""  
056ea294c256
toplevel theorem statements support 'if'/'for' eigencontext;
wenzelm
parents:
63064
diff
changeset

408 
Parse_Spec.long_statement_keyword; 
056ea294c256
toplevel theorem statements support 'if'/'for' eigencontext;
wenzelm
parents:
63064
diff
changeset

409 

056ea294c256
toplevel theorem statements support 'if'/'for' eigencontext;
wenzelm
parents:
63064
diff
changeset

410 
val long_statement = 
056ea294c256
toplevel theorem statements support 'if'/'for' eigencontext;
wenzelm
parents:
63064
diff
changeset

411 
Scan.optional (Parse_Spec.opt_thm_name ":"  Scan.ahead long_keyword) Attrib.empty_binding  
056ea294c256
toplevel theorem statements support 'if'/'for' eigencontext;
wenzelm
parents:
63064
diff
changeset

412 
Scan.optional Parse_Spec.includes []  Parse_Spec.long_statement 
056ea294c256
toplevel theorem statements support 'if'/'for' eigencontext;
wenzelm
parents:
63064
diff
changeset

413 
>> (fn ((binding, includes), (elems, concl)) => (true, binding, includes, elems, concl)); 
056ea294c256
toplevel theorem statements support 'if'/'for' eigencontext;
wenzelm
parents:
63064
diff
changeset

414 

056ea294c256
toplevel theorem statements support 'if'/'for' eigencontext;
wenzelm
parents:
63064
diff
changeset

415 
val short_statement = 
056ea294c256
toplevel theorem statements support 'if'/'for' eigencontext;
wenzelm
parents:
63064
diff
changeset

416 
Parse_Spec.statement  Parse_Spec.if_statement  Parse.for_fixes 
056ea294c256
toplevel theorem statements support 'if'/'for' eigencontext;
wenzelm
parents:
63064
diff
changeset

417 
>> (fn ((shows, assumes), fixes) => 
056ea294c256
toplevel theorem statements support 'if'/'for' eigencontext;
wenzelm
parents:
63064
diff
changeset

418 
(false, Attrib.empty_binding, [], [Element.Fixes fixes, Element.Assumes assumes], 
056ea294c256
toplevel theorem statements support 'if'/'for' eigencontext;
wenzelm
parents:
63064
diff
changeset

419 
Element.Shows shows)); 
056ea294c256
toplevel theorem statements support 'if'/'for' eigencontext;
wenzelm
parents:
63064
diff
changeset

420 

056ea294c256
toplevel theorem statements support 'if'/'for' eigencontext;
wenzelm
parents:
63064
diff
changeset

421 
fun theorem spec schematic descr = 
056ea294c256
toplevel theorem statements support 'if'/'for' eigencontext;
wenzelm
parents:
63064
diff
changeset

422 
Outer_Syntax.local_theory_to_proof' spec ("state " ^ descr) 
056ea294c256
toplevel theorem statements support 'if'/'for' eigencontext;
wenzelm
parents:
63064
diff
changeset

423 
((long_statement  short_statement) >> (fn (long, binding, includes, elems, concl) => 
056ea294c256
toplevel theorem statements support 'if'/'for' eigencontext;
wenzelm
parents:
63064
diff
changeset

424 
((if schematic then Specification.schematic_theorem_cmd else Specification.theorem_cmd) 
056ea294c256
toplevel theorem statements support 'if'/'for' eigencontext;
wenzelm
parents:
63064
diff
changeset

425 
long Thm.theoremK NONE (K I) binding includes elems concl))); 
056ea294c256
toplevel theorem statements support 'if'/'for' eigencontext;
wenzelm
parents:
63064
diff
changeset

426 

056ea294c256
toplevel theorem statements support 'if'/'for' eigencontext;
wenzelm
parents:
63064
diff
changeset

427 
val _ = theorem @{command_keyword theorem} false "theorem"; 
056ea294c256
toplevel theorem statements support 'if'/'for' eigencontext;
wenzelm
parents:
63064
diff
changeset

428 
val _ = theorem @{command_keyword lemma} false "lemma"; 
056ea294c256
toplevel theorem statements support 'if'/'for' eigencontext;
wenzelm
parents:
63064
diff
changeset

429 
val _ = theorem @{command_keyword corollary} false "corollary"; 
056ea294c256
toplevel theorem statements support 'if'/'for' eigencontext;
wenzelm
parents:
63064
diff
changeset

430 
val _ = theorem @{command_keyword proposition} false "proposition"; 
056ea294c256
toplevel theorem statements support 'if'/'for' eigencontext;
wenzelm
parents:
63064
diff
changeset

431 
val _ = theorem @{command_keyword schematic_goal} true "schematic goal"; 
056ea294c256
toplevel theorem statements support 'if'/'for' eigencontext;
wenzelm
parents:
63064
diff
changeset

432 

056ea294c256
toplevel theorem statements support 'if'/'for' eigencontext;
wenzelm
parents:
63064
diff
changeset

433 
in end\<close> 
056ea294c256
toplevel theorem statements support 'if'/'for' eigencontext;
wenzelm
parents:
63064
diff
changeset

434 

056ea294c256
toplevel theorem statements support 'if'/'for' eigencontext;
wenzelm
parents:
63064
diff
changeset

435 
ML \<open> 
056ea294c256
toplevel theorem statements support 'if'/'for' eigencontext;
wenzelm
parents:
63064
diff
changeset

436 
local 
056ea294c256
toplevel theorem statements support 'if'/'for' eigencontext;
wenzelm
parents:
63064
diff
changeset

437 

62856  438 
val _ = 
439 
Outer_Syntax.local_theory' @{command_keyword lemmas} "define theorems" 

440 
(Parse_Spec.name_facts  Parse.for_fixes >> 

441 
(fn (facts, fixes) => #2 oo Specification.theorems_cmd Thm.theoremK facts fixes)); 

442 

443 
val _ = 

444 
Outer_Syntax.local_theory' @{command_keyword declare} "declare theorems" 

62969  445 
(Parse.and_list1 Parse.thms1  Parse.for_fixes 
62856  446 
>> (fn (facts, fixes) => 
447 
#2 oo Specification.theorems_cmd "" [(Attrib.empty_binding, flat facts)] fixes)); 

448 

449 
val _ = 

450 
Outer_Syntax.local_theory @{command_keyword named_theorems} 

451 
"declare named collection of theorems" 

452 
(Parse.and_list1 (Parse.binding  Scan.optional Parse.text "") >> 

453 
fold (fn (b, descr) => snd o Named_Theorems.declare b descr)); 

454 

455 
in end\<close> 

62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

456 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

457 

62856  458 
subsubsection \<open>Hide names\<close> 
459 

460 
ML \<open> 

461 
local 

462 

463 
fun hide_names command_keyword what hide parse prep = 

464 
Outer_Syntax.command command_keyword ("hide " ^ what ^ " from name space") 

465 
((Parse.opt_keyword "open" >> not)  Scan.repeat1 parse >> (fn (fully, args) => 

466 
(Toplevel.theory (fn thy => 

467 
let val ctxt = Proof_Context.init_global thy 

468 
in fold (hide fully o prep ctxt) args thy end)))); 

469 

470 
val _ = 

471 
hide_names @{command_keyword hide_class} "classes" Sign.hide_class Parse.class 

472 
Proof_Context.read_class; 

473 

474 
val _ = 

475 
hide_names @{command_keyword hide_type} "types" Sign.hide_type Parse.type_const 

476 
((#1 o dest_Type) oo Proof_Context.read_type_name {proper = true, strict = false}); 

477 

478 
val _ = 

479 
hide_names @{command_keyword hide_const} "consts" Sign.hide_const Parse.const 

480 
((#1 o dest_Const) oo Proof_Context.read_const {proper = true, strict = false}); 

481 

482 
val _ = 

483 
hide_names @{command_keyword hide_fact} "facts" Global_Theory.hide_fact 

62969  484 
(Parse.position Parse.name) (Global_Theory.check_fact o Proof_Context.theory_of); 
62856  485 

486 
in end\<close> 

487 

488 

489 
subsection \<open>Bundled declarations\<close> 

490 

491 
ML \<open> 

492 
local 

62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

493 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

494 
val _ = 
63273  495 
Outer_Syntax.maybe_begin_local_theory @{command_keyword bundle} 
496 
"define bundle of declarations" 

62969  497 
((Parse.binding  @{keyword "="})  Parse.thms1  Parse.for_fixes 
63273  498 
>> (uncurry Bundle.bundle_cmd)) 
499 
(Parse.binding  Parse.begin >> Bundle.init); 

63270  500 

501 
val _ = 

63282  502 
Outer_Syntax.local_theory @{command_keyword unbundle} 
503 
"activate declarations from bundle in local theory" 

504 
(Scan.repeat1 (Parse.position Parse.name) >> Bundle.unbundle_cmd); 

505 

506 
val _ = 

62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

507 
Outer_Syntax.command @{command_keyword include} 
63282  508 
"activate declarations from bundle in proof body" 
62969  509 
(Scan.repeat1 (Parse.position Parse.name) >> (Toplevel.proof o Bundle.include_cmd)); 
62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

510 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

511 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

512 
Outer_Syntax.command @{command_keyword including} 
63282  513 
"activate declarations from bundle in goal refinement" 
62969  514 
(Scan.repeat1 (Parse.position Parse.name) >> (Toplevel.proof o Bundle.including_cmd)); 
62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

515 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

516 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

517 
Outer_Syntax.command @{command_keyword print_bundles} 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

518 
"print bundles of declarations" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

519 
(Parse.opt_bang >> (fn b => Toplevel.keep (Bundle.print_bundles b o Toplevel.context_of))); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

520 

62856  521 
in end\<close> 
62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

522 

62856  523 

524 
subsection \<open>Local theory specifications\<close> 

525 

526 
subsubsection \<open>Specification context\<close> 

527 

528 
ML \<open> 

529 
local 

62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

530 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

531 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

532 
Outer_Syntax.command @{command_keyword context} "begin local theory context" 
62969  533 
((Parse.position Parse.name >> (fn name => 
62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

534 
Toplevel.begin_local_theory true (Named_Target.begin name))  
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

535 
Scan.optional Parse_Spec.includes []  Scan.repeat Parse_Spec.context_element 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

536 
>> (fn (incls, elems) => Toplevel.open_target (#2 o Bundle.context_cmd incls elems))) 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

537 
 Parse.begin); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

538 

62856  539 
val _ = 
540 
Outer_Syntax.command @{command_keyword end} "end context" 

541 
(Scan.succeed 

542 
(Toplevel.exit o Toplevel.end_local_theory o Toplevel.close_target o 

543 
Toplevel.end_proof (K Proof.end_notepad))); 

62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

544 

62856  545 
in end\<close> 
546 

547 

548 
subsubsection \<open>Locales and interpretation\<close> 

549 

550 
ML \<open> 

551 
local 

62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

552 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

553 
val locale_val = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

554 
Parse_Spec.locale_expression  
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

555 
Scan.optional (@{keyword "+"}  Parse.!!! (Scan.repeat1 Parse_Spec.context_element)) []  
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

556 
Scan.repeat1 Parse_Spec.context_element >> pair ([], []); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

557 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

558 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

559 
Outer_Syntax.command @{command_keyword locale} "define named specification context" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

560 
(Parse.binding  
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

561 
Scan.optional (@{keyword "="}  Parse.!!! locale_val) (([], []), [])  Parse.opt_begin 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

562 
>> (fn ((name, (expr, elems)), begin) => 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

563 
Toplevel.begin_local_theory begin 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

564 
(Expression.add_locale_cmd name Binding.empty expr elems #> snd))); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

565 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

566 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

567 
Outer_Syntax.command @{command_keyword experiment} "open private specification context" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

568 
(Scan.repeat Parse_Spec.context_element  Parse.begin 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

569 
>> (fn elems => 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

570 
Toplevel.begin_local_theory true (Experiment.experiment_cmd elems #> snd))); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

571 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

572 
val interpretation_args = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

573 
Parse.!!! Parse_Spec.locale_expression  
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

574 
Scan.optional 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

575 
(@{keyword "rewrites"}  Parse.and_list1 (Parse_Spec.opt_thm_name ":"  Parse.prop)) []; 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

576 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

577 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

578 
Outer_Syntax.command @{command_keyword interpret} 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

579 
"prove interpretation of locale expression in proof context" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

580 
(interpretation_args >> (fn (expr, equations) => 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

581 
Toplevel.proof (Interpretation.interpret_cmd expr equations))); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

582 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

583 
val interpretation_args_with_defs = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

584 
Parse.!!! Parse_Spec.locale_expression  
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

585 
(Scan.optional (@{keyword "defines"}  Parse.and_list1 (Parse_Spec.opt_thm_name ":" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

586 
 ((Parse.binding  Parse.opt_mixfix')  @{keyword "="}  Parse.term))) []  
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

587 
Scan.optional 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

588 
(@{keyword "rewrites"}  Parse.and_list1 (Parse_Spec.opt_thm_name ":"  Parse.prop)) []); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

589 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

590 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

591 
Outer_Syntax.local_theory_to_proof @{command_keyword global_interpretation} 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

592 
"prove interpretation of locale expression into global theory" 
62856  593 
(interpretation_args_with_defs >> (fn (expr, (defs, equations)) => 
594 
Interpretation.global_interpretation_cmd expr defs equations)); 

62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

595 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

596 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

597 
Outer_Syntax.command @{command_keyword sublocale} 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

598 
"prove sublocale relation between a locale and a locale expression" 
62969  599 
((Parse.position Parse.name  (@{keyword "\<subseteq>"}  @{keyword "<"})  
62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

600 
interpretation_args_with_defs >> (fn (loc, (expr, (defs, equations))) => 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

601 
Toplevel.theory_to_proof (Interpretation.global_sublocale_cmd loc expr defs equations))) 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

602 
 interpretation_args_with_defs >> (fn (expr, (defs, equations)) => 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

603 
Toplevel.local_theory_to_proof NONE NONE (Interpretation.sublocale_cmd expr defs equations))); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

604 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

605 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

606 
Outer_Syntax.command @{command_keyword interpretation} 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

607 
"prove interpretation of locale expression in local theory or into global theory" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

608 
(interpretation_args >> (fn (expr, equations) => 
62856  609 
Toplevel.local_theory_to_proof NONE NONE 
610 
(Interpretation.isar_interpretation_cmd expr equations))); 

611 

612 
in end\<close> 

62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

613 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

614 

62856  615 
subsubsection \<open>Type classes\<close> 
62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

616 

62856  617 
ML \<open> 
618 
local 

62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

619 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

620 
val class_val = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

621 
Parse_Spec.class_expression  
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

622 
Scan.optional (@{keyword "+"}  Parse.!!! (Scan.repeat1 Parse_Spec.context_element)) []  
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

623 
Scan.repeat1 Parse_Spec.context_element >> pair []; 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

624 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

625 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

626 
Outer_Syntax.command @{command_keyword class} "define type class" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

627 
(Parse.binding  Scan.optional (@{keyword "="}  class_val) ([], [])  Parse.opt_begin 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

628 
>> (fn ((name, (supclasses, elems)), begin) => 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

629 
Toplevel.begin_local_theory begin 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

630 
(Class_Declaration.class_cmd name supclasses elems #> snd))); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

631 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

632 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

633 
Outer_Syntax.local_theory_to_proof @{command_keyword subclass} "prove a subclass relation" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

634 
(Parse.class >> Class_Declaration.subclass_cmd); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

635 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

636 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

637 
Outer_Syntax.command @{command_keyword instantiation} "instantiate and prove type arity" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

638 
(Parse.multi_arity  Parse.begin 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

639 
>> (fn arities => Toplevel.begin_local_theory true (Class.instantiation_cmd arities))); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

640 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

641 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

642 
Outer_Syntax.command @{command_keyword instance} "prove type arity or subclass relation" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

643 
((Parse.class  
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

644 
((@{keyword "\<subseteq>"}  @{keyword "<"})  Parse.!!! Parse.class) >> Class.classrel_cmd  
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

645 
Parse.multi_arity >> Class.instance_arity_cmd) >> Toplevel.theory_to_proof  
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

646 
Scan.succeed (Toplevel.local_theory_to_proof NONE NONE (Class.instantiation_instance I))); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

647 

62856  648 
in end\<close> 
62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

649 

62856  650 

651 
subsubsection \<open>Arbitrary overloading\<close> 

652 

653 
ML \<open> 

654 
local 

62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

655 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

656 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

657 
Outer_Syntax.command @{command_keyword overloading} "overloaded definitions" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

658 
(Scan.repeat1 (Parse.name  (@{keyword "=="}  @{keyword "\<equiv>"})  Parse.term  
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

659 
Scan.optional (@{keyword "("}  (@{keyword "unchecked"} >> K false)  @{keyword ")"}) true 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

660 
>> Scan.triple1)  Parse.begin 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

661 
>> (fn operations => Toplevel.begin_local_theory true (Overloading.overloading_cmd operations))); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

662 

62856  663 
in end\<close> 
62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

664 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

665 

62856  666 
subsection \<open>Proof commands\<close> 
62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

667 

62856  668 
ML \<open> 
669 
local 

62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

670 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

671 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

672 
Outer_Syntax.local_theory_to_proof @{command_keyword notepad} "begin proof context" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

673 
(Parse.begin >> K Proof.begin_notepad); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

674 

62856  675 
in end\<close> 
62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

676 

62856  677 

678 
subsubsection \<open>Statements\<close> 

679 

680 
ML \<open> 

681 
local 

62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

682 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

683 
val structured_statement = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

684 
Parse_Spec.statement  Parse_Spec.cond_statement  Parse.for_fixes 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

685 
>> (fn ((shows, (strict, assumes)), fixes) => (strict, fixes, assumes, shows)); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

686 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

687 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

688 
Outer_Syntax.command @{command_keyword have} "state local goal" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

689 
(structured_statement >> (fn (a, b, c, d) => 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

690 
Toplevel.proof' (fn int => Proof.have_cmd a NONE (K I) b c d int #> #2))); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

691 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

692 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

693 
Outer_Syntax.command @{command_keyword show} "state local goal, to refine pending subgoals" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

694 
(structured_statement >> (fn (a, b, c, d) => 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

695 
Toplevel.proof' (fn int => Proof.show_cmd a NONE (K I) b c d int #> #2))); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

696 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

697 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

698 
Outer_Syntax.command @{command_keyword hence} "oldstyle alias of \"then have\"" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

699 
(structured_statement >> (fn (a, b, c, d) => 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

700 
Toplevel.proof' (fn int => Proof.chain #> Proof.have_cmd a NONE (K I) b c d int #> #2))); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

701 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

702 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

703 
Outer_Syntax.command @{command_keyword thus} "oldstyle alias of \"then show\"" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

704 
(structured_statement >> (fn (a, b, c, d) => 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

705 
Toplevel.proof' (fn int => Proof.chain #> Proof.show_cmd a NONE (K I) b c d int #> #2))); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

706 

62856  707 
in end\<close> 
62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

708 

62856  709 

710 
subsubsection \<open>Local facts\<close> 

711 

712 
ML \<open> 

713 
local 

62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

714 

62969  715 
val facts = Parse.and_list1 Parse.thms1; 
62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

716 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

717 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

718 
Outer_Syntax.command @{command_keyword then} "forward chaining" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

719 
(Scan.succeed (Toplevel.proof Proof.chain)); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

720 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

721 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

722 
Outer_Syntax.command @{command_keyword from} "forward chaining from given facts" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

723 
(facts >> (Toplevel.proof o Proof.from_thmss_cmd)); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

724 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

725 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

726 
Outer_Syntax.command @{command_keyword with} "forward chaining from given and current facts" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

727 
(facts >> (Toplevel.proof o Proof.with_thmss_cmd)); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

728 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

729 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

730 
Outer_Syntax.command @{command_keyword note} "define facts" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

731 
(Parse_Spec.name_facts >> (Toplevel.proof o Proof.note_thmss_cmd)); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

732 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

733 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

734 
Outer_Syntax.command @{command_keyword supply} "define facts during goal refinement (unstructured)" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

735 
(Parse_Spec.name_facts >> (Toplevel.proof o Proof.supply_cmd)); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

736 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

737 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

738 
Outer_Syntax.command @{command_keyword using} "augment goal facts" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

739 
(facts >> (Toplevel.proof o Proof.using_cmd)); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

740 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

741 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

742 
Outer_Syntax.command @{command_keyword unfolding} "unfold definitions in goal and facts" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

743 
(facts >> (Toplevel.proof o Proof.unfolding_cmd)); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

744 

62856  745 
in end\<close> 
62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

746 

62856  747 

748 
subsubsection \<open>Proof context\<close> 

749 

750 
ML \<open> 

751 
local 

752 

753 
val structured_statement = 

754 
Parse_Spec.statement  Parse_Spec.if_statement'  Parse.for_fixes 

755 
>> (fn ((shows, assumes), fixes) => (fixes, assumes, shows)); 

62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

756 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

757 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

758 
Outer_Syntax.command @{command_keyword fix} "fix local variables (Skolem constants)" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

759 
(Parse.fixes >> (Toplevel.proof o Proof.fix_cmd)); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

760 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

761 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

762 
Outer_Syntax.command @{command_keyword assume} "assume propositions" 
62856  763 
(structured_statement >> (fn (a, b, c) => Toplevel.proof (Proof.assume_cmd a b c))); 
62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

764 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

765 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

766 
Outer_Syntax.command @{command_keyword presume} "assume propositions, to be established later" 
62856  767 
(structured_statement >> (fn (a, b, c) => Toplevel.proof (Proof.presume_cmd a b c))); 
62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

768 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

769 
val _ = 
63039  770 
Outer_Syntax.command @{command_keyword define} "local definition (nonpolymorphic)" 
771 
((Parse.fixes  Parse.where_)  Parse_Spec.statement  Parse.for_fixes 

772 
>> (fn ((a, b), c) => Toplevel.proof (Proof.define_cmd a c b))); 

773 

774 
val _ = 

62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

775 
Outer_Syntax.command @{command_keyword def} "local definition (nonpolymorphic)" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

776 
(Parse.and_list1 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

777 
(Parse_Spec.opt_thm_name ":"  
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

778 
((Parse.binding  Parse.opt_mixfix)  
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

779 
((@{keyword "\<equiv>"}  @{keyword "=="})  Parse.!!! Parse.termp))) 
63043  780 
>> (fn args => Toplevel.proof (fn state => 
781 
(legacy_feature "Old 'def' command  use 'define' instead"; Proof.def_cmd args state)))); 

62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

782 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

783 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

784 
Outer_Syntax.command @{command_keyword consider} "state cases rule" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

785 
(Parse_Spec.obtains >> (Toplevel.proof' o Obtain.consider_cmd)); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

786 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

787 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

788 
Outer_Syntax.command @{command_keyword obtain} "generalized elimination" 
63059
3f577308551e
'obtain' supports structured statements (similar to 'define');
wenzelm
parents:
63043
diff
changeset

789 
(Parse.parbinding  Scan.optional (Parse.fixes  Parse.where_) []  structured_statement 
3f577308551e
'obtain' supports structured statements (similar to 'define');
wenzelm
parents:
63043
diff
changeset

790 
>> (fn ((a, b), (c, d, e)) => Toplevel.proof' (Obtain.obtain_cmd a b c d e))); 
62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

791 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

792 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

793 
Outer_Syntax.command @{command_keyword guess} "wild guessing (unstructured)" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

794 
(Scan.optional Parse.fixes [] >> (Toplevel.proof' o Obtain.guess_cmd)); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

795 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

796 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

797 
Outer_Syntax.command @{command_keyword let} "bind text variables" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

798 
(Parse.and_list1 (Parse.and_list1 Parse.term  (@{keyword "="}  Parse.term)) 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

799 
>> (Toplevel.proof o Proof.let_bind_cmd)); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

800 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

801 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

802 
Outer_Syntax.command @{command_keyword write} "add concrete syntax for constants / fixed variables" 
62856  803 
(Parse.syntax_mode  Parse.and_list1 (Parse.const  Parse.mixfix) 
62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

804 
>> (fn (mode, args) => Toplevel.proof (Proof.write_cmd mode args))); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

805 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

806 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

807 
Outer_Syntax.command @{command_keyword case} "invoke local context" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

808 
(Parse_Spec.opt_thm_name ":"  
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

809 
(@{keyword "("}  
62969  810 
Parse.!!! (Parse.position Parse.name  Scan.repeat (Parse.maybe Parse.binding) 
62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

811 
 @{keyword ")"})  
62969  812 
Parse.position Parse.name >> rpair []) >> (Toplevel.proof o Proof.case_cmd)); 
62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

813 

62856  814 
in end\<close> 
62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

815 

62856  816 

817 
subsubsection \<open>Proof structure\<close> 

818 

819 
ML \<open> 

820 
local 

62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

821 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

822 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

823 
Outer_Syntax.command @{command_keyword "{"} "begin explicit proof block" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

824 
(Scan.succeed (Toplevel.proof Proof.begin_block)); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

825 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

826 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

827 
Outer_Syntax.command @{command_keyword "}"} "end explicit proof block" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

828 
(Scan.succeed (Toplevel.proof Proof.end_block)); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

829 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

830 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

831 
Outer_Syntax.command @{command_keyword next} "enter next proof block" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

832 
(Scan.succeed (Toplevel.proof Proof.next_block)); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

833 

62856  834 
in end\<close> 
62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

835 

62856  836 

837 
subsubsection \<open>End proof\<close> 

838 

839 
ML \<open> 

840 
local 

62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

841 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

842 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

843 
Outer_Syntax.command @{command_keyword qed} "conclude proof" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

844 
(Scan.option Method.parse >> (fn m => 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

845 
(Option.map Method.report m; 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

846 
Isar_Cmd.qed m))); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

847 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

848 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

849 
Outer_Syntax.command @{command_keyword by} "terminal backward proof" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

850 
(Method.parse  Scan.option Method.parse >> (fn (m1, m2) => 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

851 
(Method.report m1; 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

852 
Option.map Method.report m2; 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

853 
Isar_Cmd.terminal_proof (m1, m2)))); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

854 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

855 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

856 
Outer_Syntax.command @{command_keyword ".."} "default proof" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

857 
(Scan.succeed Isar_Cmd.default_proof); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

858 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

859 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

860 
Outer_Syntax.command @{command_keyword "."} "immediate proof" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

861 
(Scan.succeed Isar_Cmd.immediate_proof); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

862 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

863 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

864 
Outer_Syntax.command @{command_keyword done} "done proof" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

865 
(Scan.succeed Isar_Cmd.done_proof); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

866 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

867 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

868 
Outer_Syntax.command @{command_keyword sorry} "skip proof (quickanddirty mode only!)" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

869 
(Scan.succeed Isar_Cmd.skip_proof); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

870 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

871 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

872 
Outer_Syntax.command @{command_keyword "\<proof>"} "dummy proof (quickanddirty mode only!)" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

873 
(Scan.succeed Isar_Cmd.skip_proof); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

874 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

875 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

876 
Outer_Syntax.command @{command_keyword oops} "forget proof" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

877 
(Scan.succeed (Toplevel.forget_proof true)); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

878 

62856  879 
in end\<close> 
62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

880 

62856  881 

882 
subsubsection \<open>Proof steps\<close> 

883 

884 
ML \<open> 

885 
local 

62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

886 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

887 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

888 
Outer_Syntax.command @{command_keyword defer} "shuffle internal proof state" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

889 
(Scan.optional Parse.nat 1 >> (Toplevel.proof o Proof.defer)); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

890 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

891 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

892 
Outer_Syntax.command @{command_keyword prefer} "shuffle internal proof state" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

893 
(Parse.nat >> (Toplevel.proof o Proof.prefer)); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

894 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

895 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

896 
Outer_Syntax.command @{command_keyword apply} "initial goal refinement step (unstructured)" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

897 
(Method.parse >> (fn m => (Method.report m; Toplevel.proofs (Proof.apply m)))); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

898 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

899 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

900 
Outer_Syntax.command @{command_keyword apply_end} "terminal goal refinement step (unstructured)" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

901 
(Method.parse >> (fn m => (Method.report m; Toplevel.proofs (Proof.apply_end m)))); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

902 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

903 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

904 
Outer_Syntax.command @{command_keyword proof} "backward proof step" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

905 
(Scan.option Method.parse >> (fn m => 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

906 
(Option.map Method.report m; Toplevel.proofs (Proof.proof m)))); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

907 

62856  908 
in end\<close> 
62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

909 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

910 

62856  911 
subsubsection \<open>Subgoal focus\<close> 
912 

913 
ML \<open> 

62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

914 
local 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

915 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

916 
val opt_fact_binding = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

917 
Scan.optional (Parse.binding  Parse.opt_attribs  Parse.attribs >> pair Binding.empty) 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

918 
Attrib.empty_binding; 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

919 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

920 
val for_params = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

921 
Scan.optional 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

922 
(@{keyword "for"}  
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

923 
Parse.!!! ((Scan.option Parse.dots >> is_some)  
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

924 
(Scan.repeat1 (Parse.position (Parse.maybe Parse.name))))) 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

925 
(false, []); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

926 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

927 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

928 
Outer_Syntax.command @{command_keyword subgoal} 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

929 
"focus on first subgoal within backward refinement" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

930 
(opt_fact_binding  (Scan.option (@{keyword "premises"}  Parse.!!! opt_fact_binding))  
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

931 
for_params >> (fn ((a, b), c) => 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

932 
Toplevel.proofs (Seq.make_results o Seq.single o #2 o Subgoal.subgoal_cmd a b c))); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

933 

62856  934 
in end\<close> 
62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

935 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

936 

62856  937 
subsubsection \<open>Calculation\<close> 
938 

939 
ML \<open> 

940 
local 

62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

941 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

942 
val calculation_args = 
62969  943 
Scan.option (@{keyword "("}  Parse.!!! ((Parse.thms1  @{keyword ")"}))); 
62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

944 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

945 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

946 
Outer_Syntax.command @{command_keyword also} "combine calculation and current facts" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

947 
(calculation_args >> (Toplevel.proofs' o Calculation.also_cmd)); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

948 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

949 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

950 
Outer_Syntax.command @{command_keyword finally} 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

951 
"combine calculation and current facts, exhibit result" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

952 
(calculation_args >> (Toplevel.proofs' o Calculation.finally_cmd)); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

953 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

954 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

955 
Outer_Syntax.command @{command_keyword moreover} "augment calculation by current facts" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

956 
(Scan.succeed (Toplevel.proof' Calculation.moreover)); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

957 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

958 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

959 
Outer_Syntax.command @{command_keyword ultimately} 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

960 
"augment calculation by current facts, exhibit result" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

961 
(Scan.succeed (Toplevel.proof' Calculation.ultimately)); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

962 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

963 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

964 
Outer_Syntax.command @{command_keyword print_trans_rules} "print transitivity rules" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

965 
(Scan.succeed (Toplevel.keep (Calculation.print_rules o Toplevel.context_of))); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

966 

62856  967 
in end\<close> 
62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

968 

62856  969 

970 
subsubsection \<open>Proof navigation\<close> 

971 

972 
ML \<open> 

973 
local 

62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

974 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

975 
fun report_back () = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

976 
Output.report [Markup.markup Markup.bad "Explicit backtracking"]; 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

977 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

978 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

979 
Outer_Syntax.command @{command_keyword back} "explicit backtracking of proof command" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

980 
(Scan.succeed 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

981 
(Toplevel.actual_proof (fn prf => (report_back (); Proof_Node.back prf)) o 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

982 
Toplevel.skip_proof report_back)); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

983 

62856  984 
in end\<close> 
62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

985 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

986 

62856  987 
subsection \<open>Diagnostic commands (for interactive mode only)\<close> 
988 

989 
ML \<open> 

990 
local 

62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

991 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

992 
val opt_modes = 
62969  993 
Scan.optional (@{keyword "("}  Parse.!!! (Scan.repeat1 Parse.name  @{keyword ")"})) []; 
62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

994 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

995 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

996 
Outer_Syntax.command @{command_keyword help} 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

997 
"retrieve outer syntax commands according to name patterns" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

998 
(Scan.repeat Parse.name >> 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

999 
(fn pats => Toplevel.keep (fn st => Outer_Syntax.help (Toplevel.theory_of st) pats))); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1000 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1001 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1002 
Outer_Syntax.command @{command_keyword print_commands} "print outer syntax commands" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1003 
(Scan.succeed (Toplevel.keep (Outer_Syntax.print_commands o Toplevel.theory_of))); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1004 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1005 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1006 
Outer_Syntax.command @{command_keyword print_options} "print configuration options" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1007 
(Parse.opt_bang >> (fn b => Toplevel.keep (Attrib.print_options b o Toplevel.context_of))); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1008 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1009 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1010 
Outer_Syntax.command @{command_keyword print_context} 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1011 
"print context of local theory target" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1012 
(Scan.succeed (Toplevel.keep (Pretty.writeln_chunks o Toplevel.pretty_context))); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1013 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1014 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1015 
Outer_Syntax.command @{command_keyword print_theory} 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1016 
"print logical theory contents" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1017 
(Parse.opt_bang >> (fn b => 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1018 
Toplevel.keep (Pretty.writeln o Proof_Display.pretty_theory b o Toplevel.context_of))); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1019 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1020 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1021 
Outer_Syntax.command @{command_keyword print_definitions} 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1022 
"print dependencies of definitional theory content" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1023 
(Parse.opt_bang >> (fn b => 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1024 
Toplevel.keep (Pretty.writeln o Proof_Display.pretty_definitions b o Toplevel.context_of))); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1025 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1026 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1027 
Outer_Syntax.command @{command_keyword print_syntax} 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1028 
"print inner syntax of context" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1029 
(Scan.succeed (Toplevel.keep (Proof_Context.print_syntax o Toplevel.context_of))); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1030 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1031 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1032 
Outer_Syntax.command @{command_keyword print_defn_rules} 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1033 
"print definitional rewrite rules of context" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1034 
(Scan.succeed (Toplevel.keep (Local_Defs.print_rules o Toplevel.context_of))); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1035 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1036 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1037 
Outer_Syntax.command @{command_keyword print_abbrevs} 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1038 
"print constant abbreviations of context" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1039 
(Parse.opt_bang >> (fn b => 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1040 
Toplevel.keep (Proof_Context.print_abbrevs b o Toplevel.context_of))); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1041 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1042 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1043 
Outer_Syntax.command @{command_keyword print_theorems} 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1044 
"print theorems of local theory or proof context" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1045 
(Parse.opt_bang >> (fn b => 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1046 
Toplevel.keep (Pretty.writeln o Pretty.chunks o Isar_Cmd.pretty_theorems b))); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1047 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1048 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1049 
Outer_Syntax.command @{command_keyword print_locales} 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1050 
"print locales of this theory" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1051 
(Parse.opt_bang >> (fn b => 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1052 
Toplevel.keep (Locale.print_locales b o Toplevel.theory_of))); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1053 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1054 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1055 
Outer_Syntax.command @{command_keyword print_classes} 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1056 
"print classes of this theory" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1057 
(Scan.succeed (Toplevel.keep (Class.print_classes o Toplevel.context_of))); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1058 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1059 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1060 
Outer_Syntax.command @{command_keyword print_locale} 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1061 
"print locale of this theory" 
62969  1062 
(Parse.opt_bang  Parse.position Parse.name >> (fn (b, name) => 
62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1063 
Toplevel.keep (fn state => Locale.print_locale (Toplevel.theory_of state) b name))); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1064 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1065 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1066 
Outer_Syntax.command @{command_keyword print_interps} 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1067 
"print interpretations of locale for this theory or proof context" 
62969  1068 
(Parse.position Parse.name >> (fn name => 
62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1069 
Toplevel.keep (fn state => Locale.print_registrations (Toplevel.context_of state) name))); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1070 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1071 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1072 
Outer_Syntax.command @{command_keyword print_dependencies} 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1073 
"print dependencies of locale expression" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1074 
(Parse.opt_bang  Parse_Spec.locale_expression >> (fn (b, expr) => 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1075 
Toplevel.keep (fn state => Expression.print_dependencies (Toplevel.context_of state) b expr))); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1076 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1077 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1078 
Outer_Syntax.command @{command_keyword print_attributes} 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1079 
"print attributes of this theory" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1080 
(Parse.opt_bang >> (fn b => Toplevel.keep (Attrib.print_attributes b o Toplevel.context_of))); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1081 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1082 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1083 
Outer_Syntax.command @{command_keyword print_simpset} 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1084 
"print context of Simplifier" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1085 
(Parse.opt_bang >> (fn b => 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1086 
Toplevel.keep (Pretty.writeln o Simplifier.pretty_simpset b o Toplevel.context_of))); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1087 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1088 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1089 
Outer_Syntax.command @{command_keyword print_rules} "print intro/elim rules" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1090 
(Scan.succeed (Toplevel.keep (Context_Rules.print_rules o Toplevel.context_of))); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1091 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1092 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1093 
Outer_Syntax.command @{command_keyword print_methods} "print methods of this theory" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1094 
(Parse.opt_bang >> (fn b => Toplevel.keep (Method.print_methods b o Toplevel.context_of))); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1095 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1096 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1097 
Outer_Syntax.command @{command_keyword print_antiquotations} 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1098 
"print document antiquotations" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1099 
(Parse.opt_bang >> (fn b => 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1100 
Toplevel.keep (Thy_Output.print_antiquotations b o Toplevel.context_of))); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1101 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1102 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1103 
Outer_Syntax.command @{command_keyword print_ML_antiquotations} 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1104 
"print ML antiquotations" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1105 
(Parse.opt_bang >> (fn b => 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1106 
Toplevel.keep (ML_Context.print_antiquotations b o Toplevel.context_of))); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1107 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1108 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1109 
Outer_Syntax.command @{command_keyword locale_deps} "visualize locale dependencies" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1110 
(Scan.succeed 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1111 
(Toplevel.keep (Toplevel.theory_of #> (fn thy => 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1112 
Locale.pretty_locale_deps thy 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1113 
> map (fn {name, parents, body} => 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1114 
((name, Graph_Display.content_node (Locale.extern thy name) [body]), parents)) 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1115 
> Graph_Display.display_graph_old)))); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1116 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1117 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1118 
Outer_Syntax.command @{command_keyword print_term_bindings} 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1119 
"print term bindings of proof context" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1120 
(Scan.succeed 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1121 
(Toplevel.keep 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1122 
(Pretty.writeln_chunks o Proof_Context.pretty_term_bindings o Toplevel.context_of))); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1123 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1124 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1125 
Outer_Syntax.command @{command_keyword print_facts} "print facts of proof context" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1126 
(Parse.opt_bang >> (fn b => 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1127 
Toplevel.keep (Proof_Context.print_local_facts b o Toplevel.context_of))); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1128 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1129 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1130 
Outer_Syntax.command @{command_keyword print_cases} "print cases of proof context" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1131 
(Scan.succeed 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1132 
(Toplevel.keep (Pretty.writeln_chunks o Proof_Context.pretty_cases o Toplevel.context_of))); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1133 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1134 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1135 
Outer_Syntax.command @{command_keyword print_statement} 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1136 
"print theorems as long statements" 
62969  1137 
(opt_modes  Parse.thms1 >> Isar_Cmd.print_stmts); 
62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1138 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1139 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1140 
Outer_Syntax.command @{command_keyword thm} "print theorems" 
62969  1141 
(opt_modes  Parse.thms1 >> Isar_Cmd.print_thms); 
62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1142 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1143 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1144 
Outer_Syntax.command @{command_keyword prf} "print proof terms of theorems" 
62969  1145 
(opt_modes  Scan.option Parse.thms1 >> Isar_Cmd.print_prfs false); 
62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1146 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1147 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1148 
Outer_Syntax.command @{command_keyword full_prf} "print full proof terms of theorems" 
62969  1149 
(opt_modes  Scan.option Parse.thms1 >> Isar_Cmd.print_prfs true); 
62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1150 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1151 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1152 
Outer_Syntax.command @{command_keyword prop} "read and print proposition" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1153 
(opt_modes  Parse.term >> Isar_Cmd.print_prop); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1154 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1155 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1156 
Outer_Syntax.command @{command_keyword term} "read and print term" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1157 
(opt_modes  Parse.term >> Isar_Cmd.print_term); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1158 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1159 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1160 
Outer_Syntax.command @{command_keyword typ} "read and print type" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1161 
(opt_modes  (Parse.typ  Scan.option (@{keyword "::"}  Parse.!!! Parse.sort)) 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1162 
>> Isar_Cmd.print_type); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1163 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1164 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1165 
Outer_Syntax.command @{command_keyword print_codesetup} "print code generator setup" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1166 
(Scan.succeed (Toplevel.keep (Code.print_codesetup o Toplevel.theory_of))); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1167 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1168 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1169 
Outer_Syntax.command @{command_keyword print_state} 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1170 
"print current proof state (if present)" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1171 
(opt_modes >> (fn modes => 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1172 
Toplevel.keep (Print_Mode.with_modes modes (Output.state o Toplevel.string_of_state)))); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1173 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1174 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1175 
Outer_Syntax.command @{command_keyword welcome} "print welcome message" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1176 
(Scan.succeed (Toplevel.keep (fn _ => writeln (Session.welcome ())))); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1177 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1178 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1179 
Outer_Syntax.command @{command_keyword display_drafts} 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1180 
"display raw source files with symbols" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1181 
(Scan.repeat1 Parse.path >> (fn names => 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1182 
Toplevel.keep (fn _ => ignore (Present.display_drafts (map Path.explode names))))); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1183 

62856  1184 
in end\<close> 
62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1185 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1186 

62856  1187 
subsection \<open>Dependencies\<close> 
1188 

1189 
ML \<open> 

62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1190 
local 
62856  1191 

1192 
val theory_bounds = 

62969  1193 
Parse.position Parse.theory_name >> single  
1194 
(@{keyword "("}  Parse.enum "" (Parse.position Parse.theory_name)  @{keyword ")"}); 

62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1195 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1196 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1197 
Outer_Syntax.command @{command_keyword thy_deps} "visualize theory dependencies" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1198 
(Scan.option theory_bounds  Scan.option theory_bounds >> 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1199 
(fn args => Toplevel.keep (fn st => Thy_Deps.thy_deps_cmd (Toplevel.context_of st) args))); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1200 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1201 

62856  1202 
val class_bounds = 
1203 
Parse.sort >> single  

1204 
(@{keyword "("}  Parse.enum "" Parse.sort  @{keyword ")"}); 

62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1205 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1206 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1207 
Outer_Syntax.command @{command_keyword class_deps} "visualize class dependencies" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1208 
(Scan.option class_bounds  Scan.option class_bounds >> (fn args => 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1209 
Toplevel.keep (fn st => Class_Deps.class_deps_cmd (Toplevel.context_of st) args))); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1210 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1211 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1212 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1213 
Outer_Syntax.command @{command_keyword thm_deps} "visualize theorem dependencies" 
62969  1214 
(Parse.thms1 >> (fn args => 
62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1215 
Toplevel.keep (fn st => 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1216 
Thm_Deps.thm_deps (Toplevel.theory_of st) 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1217 
(Attrib.eval_thms (Toplevel.context_of st) args)))); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1218 

62856  1219 

1220 
val thy_names = 

62969  1221 
Scan.repeat1 (Scan.unless Parse.minus (Parse.position Parse.theory_name)); 
62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1222 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1223 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1224 
Outer_Syntax.command @{command_keyword unused_thms} "find unused theorems" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1225 
(Scan.option ((thy_names  Parse.minus)  Scan.option thy_names) >> (fn opt_range => 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1226 
Toplevel.keep (fn st => 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1227 
let 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1228 
val thy = Toplevel.theory_of st; 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1229 
val ctxt = Toplevel.context_of st; 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1230 
fun pretty_thm (a, th) = Proof_Context.pretty_fact ctxt (a, [th]); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1231 
val check = Theory.check ctxt; 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1232 
in 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1233 
Thm_Deps.unused_thms 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1234 
(case opt_range of 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1235 
NONE => (Theory.parents_of thy, [thy]) 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1236 
 SOME (xs, NONE) => (map check xs, [thy]) 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1237 
 SOME (xs, SOME ys) => (map check xs, map check ys)) 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1238 
> map pretty_thm > Pretty.writeln_chunks 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1239 
end))); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1240 

62856  1241 
in end\<close> 
62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1242 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1243 

62856  1244 
subsubsection \<open>Find consts and theorems\<close> 
1245 

1246 
ML \<open> 

1247 
local 

62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1248 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1249 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1250 
Outer_Syntax.command @{command_keyword find_consts} 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1251 
"find constants by name / type patterns" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1252 
(Find_Consts.query_parser >> (fn spec => 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1253 
Toplevel.keep (fn st => 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1254 
Pretty.writeln (Find_Consts.pretty_consts (Toplevel.context_of st) spec)))); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1255 

62856  1256 
val options = 
1257 
Scan.optional 

1258 
(Parse.$$$ "("  

1259 
Parse.!!! (Scan.option Parse.nat  

1260 
Scan.optional (Parse.reserved "with_dups" >> K false) true  Parse.$$$ ")")) 

1261 
(NONE, true); 

62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1262 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1263 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1264 
Outer_Syntax.command @{command_keyword find_theorems} 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1265 
"find theorems meeting specified criteria" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1266 
(options  Find_Theorems.query_parser >> (fn ((opt_lim, rem_dups), spec) => 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1267 
Toplevel.keep (fn st => 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1268 
Pretty.writeln 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1269 
(Find_Theorems.pretty_theorems (Find_Theorems.proof_state st) opt_lim rem_dups spec)))); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1270 

62856  1271 
in end\<close> 
62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1272 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1273 

62856  1274 
subsection \<open>Code generation\<close> 
62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1275 

62856  1276 
ML \<open> 
1277 
local 

1278 

1279 
val _ = 

1280 
Outer_Syntax.command @{command_keyword code_datatype} 

1281 
"define set of code datatype constructors" 

1282 
(Scan.repeat1 Parse.term >> (Toplevel.theory o Code.add_datatype_cmd)); 

1283 

1284 
in end\<close> 

1285 

1286 

1287 
subsection \<open>Extraction of programs from proofs\<close> 

1288 

1289 
ML \<open> 

1290 
local 

62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1291 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1292 
val parse_vars = Scan.optional (Parse.$$$ "("  Parse.list1 Parse.name  Parse.$$$ ")") []; 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1293 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1294 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1295 
Outer_Syntax.command @{command_keyword realizers} 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1296 
"specify realizers for primitive axioms / theorems, together with correctness proof" 
62969  1297 
(Scan.repeat1 (Parse.name  parse_vars  Parse.$$$ ":"  Parse.string  Parse.string) >> 
62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1298 
(fn xs => Toplevel.theory (fn thy => Extraction.add_realizers 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1299 
(map (fn (((a, vs), s1), s2) => (Global_Theory.get_thm thy a, (vs, s1, s2))) xs) thy))); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1300 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1301 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1302 
Outer_Syntax.command @{command_keyword realizability} 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1303 
"add equations characterizing realizability" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1304 
(Scan.repeat1 Parse.string >> (Toplevel.theory o Extraction.add_realizes_eqns)); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1305 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1306 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1307 
Outer_Syntax.command @{command_keyword extract_type} 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1308 
"add equations characterizing type of extracted program" 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1309 
(Scan.repeat1 Parse.string >> (Toplevel.theory o Extraction.add_typeof_eqns)); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1310 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1311 
val _ = 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1312 
Outer_Syntax.command @{command_keyword extract} "extract terms from proofs" 
62969  1313 
(Scan.repeat1 (Parse.name  parse_vars) >> (fn xs => Toplevel.theory (fn thy => 
62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1314 
Extraction.extract (map (apfst (Global_Theory.get_thm thy)) xs) thy))); 
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1315 

62856  1316 
in end\<close> 
62849
caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1317 

caaa2fc4040d
clarified bootstrap  avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset

1318 

62944
3ee643c5ed00
more standard session build process, including browser_ 