author  wenzelm 
Thu, 04 Jun 2009 18:00:47 +0200  
changeset 31432  9858f32f9569 
parent 31335  ba5b7749fa61 
child 31476  c5d2899b6de9 
permissions  rwrr 
31432
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

1 
(** Pure Isabelle **) 
0  2 

26109
c69c3559355b
more elaborate structure Distribution (filledin by makedist);
wenzelm
parents:
25953
diff
changeset

3 
structure Distribution = (*filledin by makedist*) 
c69c3559355b
more elaborate structure Distribution (filledin by makedist);
wenzelm
parents:
25953
diff
changeset

4 
struct 
c69c3559355b
more elaborate structure Distribution (filledin by makedist);
wenzelm
parents:
25953
diff
changeset

5 
val version = "Isabelle repository version"; 
27642
c0db1220b071
structure Distribution: swapped default for is_official;
wenzelm
parents:
27546
diff
changeset

6 
val is_official = false; 
c0db1220b071
structure Distribution: swapped default for is_official;
wenzelm
parents:
27546
diff
changeset

7 
val changelog = ""; 
26109
c69c3559355b
more elaborate structure Distribution (filledin by makedist);
wenzelm
parents:
25953
diff
changeset

8 
end; 
11835  9 

23825
e0372eba47b7
simplified loading of ML files  no static forward references;
wenzelm
parents:
23696
diff
changeset

10 
(*if true then some tools will OMIT some proofs*) 
e0372eba47b7
simplified loading of ML files  no static forward references;
wenzelm
parents:
23696
diff
changeset

11 
val quick_and_dirty = ref false; 
e0372eba47b7
simplified loading of ML files  no static forward references;
wenzelm
parents:
23696
diff
changeset

12 

12248  13 
print_depth 10; 
0  14 

31432
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

15 

9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

16 
(* library of general tools *) 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

17 

21396  18 
use "General/basics.ML"; 
0  19 
use "library.ML"; 
31432
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

20 
use "General/print_mode.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

21 
use "General/alist.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

22 
use "General/table.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

23 
use "General/output.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

24 
use "General/properties.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

25 
use "General/markup.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

26 
use "General/scan.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

27 
use "General/source.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

28 
use "General/symbol.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

29 
use "General/seq.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

30 
use "General/position.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

31 
use "General/symbol_pos.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

32 
use "General/antiquote.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

33 
use "ML/ml_lex.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

34 
use "ML/ml_parse.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

35 
use "General/secure.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

36 
(* basic ML bootstrap finished *) 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

37 
use "General/integer.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

38 
use "General/stack.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

39 
use "General/queue.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

40 
use "General/heap.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

41 
use "General/ord_list.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

42 
use "General/balanced_tree.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

43 
use "General/graph.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

44 
use "General/long_name.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

45 
use "General/binding.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

46 
use "General/name_space.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

47 
use "General/lazy.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

48 
use "General/path.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

49 
use "General/url.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

50 
use "General/buffer.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

51 
use "General/file.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

52 
use "General/xml.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

53 
use "General/yxml.ML"; 
22592  54 

31432
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

55 

9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

56 
(* concurrency within the ML runtime *) 
28120  57 

31432
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

58 
use "Concurrent/simple_thread.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

59 
use "Concurrent/synchronized.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

60 
use "Concurrent/mailbox.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

61 
use "Concurrent/task_queue.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

62 
use "Concurrent/future.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

63 
use "Concurrent/par_list.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

64 
if Multithreading.available then () else use "Concurrent/par_list_dummy.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

65 

9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

66 

9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

67 
(* fundamental structures *) 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

68 

20075  69 
use "name.ML"; 
0  70 
use "term.ML"; 
29269
5c25a2012975
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
29263
diff
changeset

71 
use "term_ord.ML"; 
20507  72 
use "term_subst.ML"; 
29263  73 
use "old_term.ML"; 
24257  74 
use "logic.ML"; 
14823
ebb8499d0fd2
moved print_mode to General/output.ML; load General/pretty.ML early;
wenzelm
parents:
14781
diff
changeset

75 
use "General/pretty.ML"; 
28404  76 
use "context.ML"; 
77 
use "context_position.ML"; 

24235  78 
use "Syntax/lexicon.ML"; 
79 
use "Syntax/simple_syntax.ML"; 

24272  80 
use "sorts.ML"; 
81 
use "type.ML"; 

24113  82 
use "config.ML"; 
19  83 

31432
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

84 

9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

85 
(* inner syntax *) 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

86 

22679  87 
use "Syntax/ast.ML"; 
88 
use "Syntax/syn_ext.ML"; 

89 
use "Syntax/parser.ML"; 

90 
use "Syntax/type_ext.ML"; 

91 
use "Syntax/syn_trans.ML"; 

92 
use "Syntax/mixfix.ML"; 

93 
use "Syntax/printer.ML"; 

94 
use "Syntax/syntax.ML"; 

95 

27262  96 
use "type_infer.ML"; 
31326
deddd77112b7
slightly later setup of ML and secure operations;
wenzelm
parents:
30834
diff
changeset

97 

31432
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

98 

9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

99 
(* core of tactical proof system *) 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

100 

30559
e5987a7ac5df
turned structure NetRules into general Item_Net, which is loaded earlier;
wenzelm
parents:
30173
diff
changeset

101 
use "net.ML"; 
e5987a7ac5df
turned structure NetRules into general Item_Net, which is loaded earlier;
wenzelm
parents:
30173
diff
changeset

102 
use "item_net.ML"; 
18934  103 
use "envir.ML"; 
18059  104 
use "consts.ML"; 
24257  105 
use "primitive_defs.ML"; 
27546  106 
use "defs.ML"; 
0  107 
use "sign.ML"; 
108 
use "pattern.ML"; 

109 
use "unify.ML"; 

1528  110 
use "theory.ML"; 
24664  111 
use "interpretation.ML"; 
11511  112 
use "proofterm.ML"; 
0  113 
use "thm.ML"; 
22361  114 
use "more_thm.ML"; 
26279  115 
use "facts.ML"; 
3986  116 
use "pure_thy.ML"; 
19589  117 
use "display.ML"; 
0  118 
use "drule.ML"; 
22233  119 
use "morphism.ML"; 
19898  120 
use "variable.ML"; 
24833  121 
use "conv.ML"; 
0  122 
use "tctical.ML"; 
1582  123 
use "search.ML"; 
21708  124 
use "tactic.ML"; 
15006
107e4dfd3b96
Merging the metasimplifier with the Proverssimplifier. Next step:
skalberg
parents:
14823
diff
changeset

125 
use "meta_simplifier.ML"; 
19417  126 
use "conjunction.ML"; 
20225  127 
use "assumption.ML"; 
17963  128 
use "goal.ML"; 
24963  129 
use "axclass.ML"; 
0  130 

31432
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

131 

9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

132 
(* Isar  Intelligible SemiAutomated Reasoning *) 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

133 

9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

134 
(*proof context*) 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

135 
use "Isar/object_logic.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

136 
use "Isar/rule_cases.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

137 
use "Isar/auto_bind.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

138 
use "Isar/local_syntax.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

139 
use "Isar/proof_context.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

140 
use "Isar/local_defs.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

141 

9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

142 
(*proof term operations*) 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

143 
use "Proof/reconstruct.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

144 
use "Proof/proof_syntax.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

145 
use "Proof/proof_rewrite_rules.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

146 
use "Proof/proofchecker.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

147 

9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

148 
(*outer syntax*) 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

149 
use "Isar/outer_lex.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

150 
use "Isar/outer_keyword.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

151 
use "Isar/outer_parse.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

152 
use "Isar/value_parse.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

153 
use "Isar/args.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

154 

9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

155 
(*ML support*) 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

156 
use "ML/ml_syntax.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

157 
use "ML/ml_env.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

158 
if ml_system = "polymlexperimental" 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

159 
then use "ML/ml_compiler_polyml5.3.ML" 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

160 
else use "ML/ml_compiler.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

161 
use "ML/ml_context.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

162 

9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

163 
(*theory sources*) 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

164 
use "Thy/thy_header.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

165 
use "Thy/thy_load.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

166 
use "Thy/html.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

167 
use "Thy/latex.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

168 
use "Thy/present.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

169 

9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

170 
(*basic proof engine*) 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

171 
use "Isar/proof_display.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

172 
use "Isar/attrib.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

173 
use "ML/ml_antiquote.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

174 
use "Isar/context_rules.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

175 
use "Isar/skip_proof.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

176 
use "Isar/method.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

177 
use "Isar/proof.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

178 
use "ML/ml_thms.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

179 
use "Isar/element.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

180 

9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

181 
(*derived theory and proof elements*) 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

182 
use "Isar/calculation.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

183 
use "Isar/obtain.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

184 

9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

185 
(*local theories and targets*) 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

186 
use "Isar/local_theory.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

187 
use "Isar/overloading.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

188 
use "Isar/locale.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

189 
use "Isar/class_target.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

190 
use "Isar/theory_target.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

191 
use "Isar/expression.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

192 
use "Isar/class.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

193 

9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

194 
use "simplifier.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

195 

9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

196 
(*executable theory content*) 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

197 
use "Isar/code.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

198 

9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

199 
(*specifications*) 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

200 
use "Isar/spec_parse.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

201 
use "Isar/specification.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

202 
use "Isar/constdefs.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

203 

9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

204 
(*toplevel transactions*) 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

205 
use "Isar/proof_node.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

206 
use "Isar/toplevel.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

207 

9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

208 
(*theory syntax*) 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

209 
use "Thy/term_style.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

210 
use "Thy/thy_output.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

211 
use "Thy/thy_syntax.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

212 
use "old_goals.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

213 
use "Isar/outer_syntax.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

214 
use "Thy/thy_info.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

215 
use "Isar/isar_document.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

216 

9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

217 
(*theory and proof operations*) 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

218 
use "Isar/rule_insts.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

219 
use "Thy/thm_deps.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

220 
use "Isar/isar_cmd.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

221 
use "Isar/isar_syn.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

222 

20207  223 
use "subgoal.ML"; 
5834  224 

13402  225 
use "Proof/extraction.ML"; 
11511  226 

31432
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

227 

9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

228 
(* Isabelle/Isar system *) 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

229 

30173
eabece26b89b
moved isabelle_process.ML, isabelle_process.scala, isar.ML, session.ML to Pure/System/ (together with associated Isar commands);
wenzelm
parents:
29269
diff
changeset

230 
use "System/session.ML"; 
eabece26b89b
moved isabelle_process.ML, isabelle_process.scala, isar.ML, session.ML to Pure/System/ (together with associated Isar commands);
wenzelm
parents:
29269
diff
changeset

231 
use "System/isar.ML"; 
eabece26b89b
moved isabelle_process.ML, isabelle_process.scala, isar.ML, session.ML to Pure/System/ (together with associated Isar commands);
wenzelm
parents:
29269
diff
changeset

232 
use "System/isabelle_process.ML"; 
eabece26b89b
moved isabelle_process.ML, isabelle_process.scala, isar.ML, session.ML to Pure/System/ (together with associated Isar commands);
wenzelm
parents:
29269
diff
changeset

233 

31432
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

234 

9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

235 
(* miscellaneous tools and packages for Pure Isabelle *) 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

236 

9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

237 
use "Tools/named_thms.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

238 

9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

239 
use "Tools/xml_syntax.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

240 

9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

241 
use "Tools/find_theorems.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

242 
use "Tools/find_consts.ML"; 
17467  243 

24455  244 
use "codegen.ML"; 
245 

31432
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

246 

9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

247 
(* configuration for Proof General *) 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

248 

9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

249 
use "ProofGeneral/pgip_types.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

250 
use "ProofGeneral/pgml.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

251 
use "ProofGeneral/pgip_markup.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

252 
use "ProofGeneral/pgip_input.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

253 
use "ProofGeneral/pgip_output.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

254 
use "ProofGeneral/pgip.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

255 

9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

256 
use "ProofGeneral/pgip_isabelle.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

257 

9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

258 
use "ProofGeneral/preferences.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

259 

9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

260 
use "ProofGeneral/pgip_parser.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

261 

9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

262 
use "ProofGeneral/pgip_tests.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

263 

9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

264 
use "ProofGeneral/proof_general_pgip.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

265 
use "ProofGeneral/proof_general_emacs.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

266 

16781  267 

23825
e0372eba47b7
simplified loading of ML files  no static forward references;
wenzelm
parents:
23696
diff
changeset

268 
use "pure_setup.ML"; 
30639
fe40d740d7c1
ML/ml_test.ML: test of advanced ML compiler invocation in Poly/ML 5.3;
wenzelm
parents:
30559
diff
changeset

269 