author | wenzelm |
Mon, 18 Apr 2011 11:13:29 +0200 | |
changeset 43258 | 0ae4ad40d7b5 |
parent 43257 | dcd983ee2c29 |
child 43286 | 13ecdb3057d8 |
permissions | -rw-r--r-- |
wenzelm@31436 | 1 |
(** Pure Isabelle **) |
clasohm@0 | 2 |
|
wenzelm@26109 | 3 |
structure Distribution = (*filled-in by makedist*) |
wenzelm@26109 | 4 |
struct |
wenzelm@32361 | 5 |
val version = "unidentified repository version"; |
wenzelm@27642 | 6 |
val is_official = false; |
wenzelm@27642 | 7 |
val changelog = ""; |
wenzelm@26109 | 8 |
end; |
wenzelm@11835 | 9 |
|
wenzelm@23825 | 10 |
(*if true then some tools will OMIT some proofs*) |
wenzelm@32738 | 11 |
val quick_and_dirty = Unsynchronized.ref false; |
wenzelm@23825 | 12 |
|
wenzelm@12248 | 13 |
print_depth 10; |
clasohm@0 | 14 |
|
wenzelm@31436 | 15 |
|
wenzelm@31436 | 16 |
(* library of general tools *) |
wenzelm@31436 | 17 |
|
wenzelm@21396 | 18 |
use "General/basics.ML"; |
clasohm@0 | 19 |
use "library.ML"; |
wenzelm@31436 | 20 |
use "General/print_mode.ML"; |
wenzelm@31436 | 21 |
use "General/alist.ML"; |
wenzelm@31436 | 22 |
use "General/table.ML"; |
wenzelm@31436 | 23 |
use "General/output.ML"; |
wenzelm@42883 | 24 |
use "General/timing.ML"; |
wenzelm@31436 | 25 |
use "General/properties.ML"; |
wenzelm@31436 | 26 |
use "General/markup.ML"; |
wenzelm@31436 | 27 |
use "General/scan.ML"; |
wenzelm@31436 | 28 |
use "General/source.ML"; |
wenzelm@31436 | 29 |
use "General/symbol.ML"; |
wenzelm@31436 | 30 |
use "General/seq.ML"; |
wenzelm@31436 | 31 |
use "General/position.ML"; |
wenzelm@31436 | 32 |
use "General/symbol_pos.ML"; |
wenzelm@31436 | 33 |
use "General/antiquote.ML"; |
wenzelm@31436 | 34 |
use "ML/ml_lex.ML"; |
wenzelm@31436 | 35 |
use "ML/ml_parse.ML"; |
wenzelm@31436 | 36 |
use "General/secure.ML"; |
wenzelm@32015 | 37 |
(*^^^^^ end of basic ML bootstrap ^^^^^*) |
wenzelm@31436 | 38 |
use "General/integer.ML"; |
wenzelm@31436 | 39 |
use "General/stack.ML"; |
wenzelm@31436 | 40 |
use "General/queue.ML"; |
wenzelm@31436 | 41 |
use "General/heap.ML"; |
wenzelm@32015 | 42 |
use "General/same.ML"; |
wenzelm@31436 | 43 |
use "General/ord_list.ML"; |
wenzelm@31436 | 44 |
use "General/balanced_tree.ML"; |
wenzelm@31436 | 45 |
use "General/graph.ML"; |
wenzelm@38708 | 46 |
use "General/linear_set.ML"; |
wenzelm@31436 | 47 |
use "General/long_name.ML"; |
wenzelm@31436 | 48 |
use "General/binding.ML"; |
wenzelm@31436 | 49 |
use "General/path.ML"; |
wenzelm@31436 | 50 |
use "General/url.ML"; |
wenzelm@31436 | 51 |
use "General/buffer.ML"; |
wenzelm@31436 | 52 |
use "General/file.ML"; |
wenzelm@31436 | 53 |
use "General/xml.ML"; |
wenzelm@38564 | 54 |
use "General/xml_data.ML"; |
wenzelm@31436 | 55 |
use "General/yxml.ML"; |
wenzelm@43258 | 56 |
use "General/pretty.ML"; |
wenzelm@22592 | 57 |
|
wenzelm@35628 | 58 |
use "General/sha1.ML"; |
wenzelm@35628 | 59 |
if String.isPrefix "polyml" ml_system |
wenzelm@35628 | 60 |
then use "General/sha1_polyml.ML" |
wenzelm@35628 | 61 |
else (); |
wenzelm@35628 | 62 |
|
wenzelm@28120 | 63 |
|
wenzelm@31436 | 64 |
(* concurrency within the ML runtime *) |
wenzelm@31436 | 65 |
|
wenzelm@31436 | 66 |
use "Concurrent/simple_thread.ML"; |
wenzelm@32844 | 67 |
|
wenzelm@35014 | 68 |
use "Concurrent/single_assignment.ML"; |
wenzelm@35014 | 69 |
if Multithreading.available then () |
wenzelm@35014 | 70 |
else use "Concurrent/single_assignment_sequential.ML"; |
wenzelm@35014 | 71 |
|
wenzelm@31436 | 72 |
use "Concurrent/synchronized.ML"; |
wenzelm@32825 | 73 |
if Multithreading.available then () |
wenzelm@32825 | 74 |
else use "Concurrent/synchronized_sequential.ML"; |
wenzelm@32844 | 75 |
|
wenzelm@42598 | 76 |
if String.isPrefix "smlnj" ml_system then () |
wenzelm@42598 | 77 |
else use "Concurrent/time_limit.ML"; |
wenzelm@42581 | 78 |
|
wenzelm@41001 | 79 |
if Multithreading.available |
wenzelm@41001 | 80 |
then use "Concurrent/bash.ML" |
wenzelm@41001 | 81 |
else use "Concurrent/bash_sequential.ML"; |
wenzelm@41001 | 82 |
|
wenzelm@41001 | 83 |
fun bash s = |
wenzelm@41001 | 84 |
(case bash_output s of |
wenzelm@41001 | 85 |
("", rc) => rc |
wenzelm@41001 | 86 |
| (out, rc) => (writeln (perhaps (try (unsuffix "\n")) out); rc)); |
wenzelm@41001 | 87 |
|
wenzelm@31436 | 88 |
use "Concurrent/mailbox.ML"; |
wenzelm@31436 | 89 |
use "Concurrent/task_queue.ML"; |
wenzelm@31436 | 90 |
use "Concurrent/future.ML"; |
wenzelm@32844 | 91 |
|
wenzelm@32824 | 92 |
use "Concurrent/lazy.ML"; |
wenzelm@32824 | 93 |
if Multithreading.available then () |
wenzelm@32824 | 94 |
else use "Concurrent/lazy_sequential.ML"; |
wenzelm@32844 | 95 |
|
wenzelm@31436 | 96 |
use "Concurrent/par_list.ML"; |
wenzelm@32824 | 97 |
if Multithreading.available then () |
wenzelm@32825 | 98 |
else use "Concurrent/par_list_sequential.ML"; |
wenzelm@31436 | 99 |
|
wenzelm@32844 | 100 |
use "Concurrent/cache.ML"; |
wenzelm@32844 | 101 |
|
wenzelm@31436 | 102 |
|
wenzelm@31436 | 103 |
(* fundamental structures *) |
wenzelm@31436 | 104 |
|
wenzelm@20075 | 105 |
use "name.ML"; |
clasohm@0 | 106 |
use "term.ML"; |
wenzelm@28404 | 107 |
use "context.ML"; |
wenzelm@39777 | 108 |
use "config.ML"; |
wenzelm@28404 | 109 |
use "context_position.ML"; |
wenzelm@19 | 110 |
|
wenzelm@31436 | 111 |
|
wenzelm@31436 | 112 |
(* inner syntax *) |
wenzelm@31436 | 113 |
|
wenzelm@43142 | 114 |
use "Syntax/term_position.ML"; |
wenzelm@43142 | 115 |
use "Syntax/lexicon.ML"; |
wenzelm@22679 | 116 |
use "Syntax/ast.ML"; |
wenzelm@43160 | 117 |
use "Syntax/syntax_ext.ML"; |
wenzelm@22679 | 118 |
use "Syntax/parser.ML"; |
wenzelm@43156 | 119 |
use "Syntax/syntax_trans.ML"; |
wenzelm@22679 | 120 |
use "Syntax/mixfix.ML"; |
wenzelm@22679 | 121 |
use "Syntax/printer.ML"; |
wenzelm@22679 | 122 |
use "Syntax/syntax.ML"; |
wenzelm@22679 | 123 |
|
wenzelm@31436 | 124 |
|
wenzelm@31436 | 125 |
(* core of tactical proof system *) |
wenzelm@31436 | 126 |
|
wenzelm@43257 | 127 |
use "term_ord.ML"; |
wenzelm@43257 | 128 |
use "term_subst.ML"; |
wenzelm@43257 | 129 |
use "old_term.ML"; |
wenzelm@43257 | 130 |
use "General/name_space.ML"; |
wenzelm@43257 | 131 |
use "sorts.ML"; |
wenzelm@43257 | 132 |
use "type.ML"; |
wenzelm@43257 | 133 |
use "logic.ML"; |
wenzelm@43257 | 134 |
use "Syntax/simple_syntax.ML"; |
wenzelm@30561 | 135 |
use "net.ML"; |
wenzelm@30561 | 136 |
use "item_net.ML"; |
wenzelm@18934 | 137 |
use "envir.ML"; |
wenzelm@18059 | 138 |
use "consts.ML"; |
wenzelm@24257 | 139 |
use "primitive_defs.ML"; |
haftmann@27546 | 140 |
use "defs.ML"; |
clasohm@0 | 141 |
use "sign.ML"; |
clasohm@0 | 142 |
use "pattern.ML"; |
clasohm@0 | 143 |
use "unify.ML"; |
paulson@1528 | 144 |
use "theory.ML"; |
wenzelm@24664 | 145 |
use "interpretation.ML"; |
berghofe@11511 | 146 |
use "proofterm.ML"; |
clasohm@0 | 147 |
use "thm.ML"; |
wenzelm@22361 | 148 |
use "more_thm.ML"; |
wenzelm@26279 | 149 |
use "facts.ML"; |
wenzelm@39814 | 150 |
use "global_theory.ML"; |
wenzelm@3986 | 151 |
use "pure_thy.ML"; |
clasohm@0 | 152 |
use "drule.ML"; |
wenzelm@22233 | 153 |
use "morphism.ML"; |
wenzelm@19898 | 154 |
use "variable.ML"; |
wenzelm@24833 | 155 |
use "conv.ML"; |
wenzelm@32187 | 156 |
use "goal_display.ML"; |
wenzelm@32169 | 157 |
use "tactical.ML"; |
paulson@1582 | 158 |
use "search.ML"; |
wenzelm@21708 | 159 |
use "tactic.ML"; |
wenzelm@41494 | 160 |
use "raw_simplifier.ML"; |
wenzelm@19417 | 161 |
use "conjunction.ML"; |
wenzelm@20225 | 162 |
use "assumption.ML"; |
wenzelm@32109 | 163 |
use "display.ML"; |
wenzelm@17963 | 164 |
use "goal.ML"; |
clasohm@0 | 165 |
|
wenzelm@31436 | 166 |
|
wenzelm@31436 | 167 |
(* Isar -- Intelligible Semi-Automated Reasoning *) |
wenzelm@31436 | 168 |
|
wenzelm@31436 | 169 |
(*proof context*) |
wenzelm@31436 | 170 |
use "Isar/object_logic.ML"; |
wenzelm@31436 | 171 |
use "Isar/rule_cases.ML"; |
wenzelm@31436 | 172 |
use "Isar/auto_bind.ML"; |
wenzelm@43116 | 173 |
use "type_infer.ML"; |
wenzelm@43115 | 174 |
use "Syntax/local_syntax.ML"; |
wenzelm@31436 | 175 |
use "Isar/proof_context.ML"; |
wenzelm@43118 | 176 |
use "Syntax/syntax_phases.ML"; |
wenzelm@31436 | 177 |
use "Isar/local_defs.ML"; |
wenzelm@31436 | 178 |
|
wenzelm@31436 | 179 |
(*proof term operations*) |
wenzelm@31436 | 180 |
use "Proof/reconstruct.ML"; |
wenzelm@31436 | 181 |
use "Proof/proof_syntax.ML"; |
wenzelm@31436 | 182 |
use "Proof/proof_rewrite_rules.ML"; |
wenzelm@31436 | 183 |
use "Proof/proofchecker.ML"; |
wenzelm@31436 | 184 |
|
wenzelm@31436 | 185 |
(*outer syntax*) |
wenzelm@36969 | 186 |
use "Isar/token.ML"; |
wenzelm@36949 | 187 |
use "Isar/keyword.ML"; |
wenzelm@36949 | 188 |
use "Isar/parse.ML"; |
wenzelm@36951 | 189 |
use "Isar/parse_value.ML"; |
wenzelm@31436 | 190 |
use "Isar/args.ML"; |
wenzelm@31436 | 191 |
|
wenzelm@31436 | 192 |
(*ML support*) |
wenzelm@31436 | 193 |
use "ML/ml_syntax.ML"; |
wenzelm@31436 | 194 |
use "ML/ml_env.ML"; |
wenzelm@31476 | 195 |
use "Isar/runtime.ML"; |
wenzelm@39200 | 196 |
use "ML/ml_compiler.ML"; |
wenzelm@42598 | 197 |
if ml_system = "polyml-5.2.1" orelse String.isPrefix "smlnj" ml_system then () |
wenzelm@38788 | 198 |
else use "ML/ml_compiler_polyml-5.3.ML"; |
wenzelm@31436 | 199 |
use "ML/ml_context.ML"; |
wenzelm@31436 | 200 |
|
wenzelm@31436 | 201 |
(*theory sources*) |
wenzelm@31436 | 202 |
use "Thy/thy_header.ML"; |
wenzelm@31436 | 203 |
use "Thy/html.ML"; |
wenzelm@31436 | 204 |
use "Thy/latex.ML"; |
wenzelm@31436 | 205 |
|
wenzelm@31436 | 206 |
(*basic proof engine*) |
wenzelm@31436 | 207 |
use "Isar/proof_display.ML"; |
wenzelm@31436 | 208 |
use "Isar/attrib.ML"; |
wenzelm@31436 | 209 |
use "ML/ml_antiquote.ML"; |
wenzelm@31436 | 210 |
use "Isar/context_rules.ML"; |
wenzelm@31436 | 211 |
use "Isar/skip_proof.ML"; |
wenzelm@31436 | 212 |
use "Isar/method.ML"; |
wenzelm@31436 | 213 |
use "Isar/proof.ML"; |
wenzelm@31436 | 214 |
use "ML/ml_thms.ML"; |
wenzelm@31436 | 215 |
use "Isar/element.ML"; |
wenzelm@31436 | 216 |
|
wenzelm@31436 | 217 |
(*derived theory and proof elements*) |
wenzelm@31436 | 218 |
use "Isar/calculation.ML"; |
wenzelm@31436 | 219 |
use "Isar/obtain.ML"; |
wenzelm@31436 | 220 |
|
wenzelm@31436 | 221 |
(*local theories and targets*) |
wenzelm@31436 | 222 |
use "Isar/local_theory.ML"; |
haftmann@38577 | 223 |
use "Isar/locale.ML"; |
haftmann@38531 | 224 |
use "Isar/generic_target.ML"; |
wenzelm@31436 | 225 |
use "Isar/overloading.ML"; |
wenzelm@35676 | 226 |
use "axclass.ML"; |
haftmann@38605 | 227 |
use "Isar/class.ML"; |
haftmann@38586 | 228 |
use "Isar/named_target.ML"; |
wenzelm@31436 | 229 |
use "Isar/expression.ML"; |
haftmann@38605 | 230 |
use "Isar/class_declaration.ML"; |
wenzelm@31436 | 231 |
|
wenzelm@31436 | 232 |
use "simplifier.ML"; |
wenzelm@31436 | 233 |
|
wenzelm@31436 | 234 |
(*executable theory content*) |
wenzelm@31436 | 235 |
use "Isar/code.ML"; |
wenzelm@31436 | 236 |
|
wenzelm@31436 | 237 |
(*specifications*) |
wenzelm@36952 | 238 |
use "Isar/parse_spec.ML"; |
wenzelm@33374 | 239 |
use "Isar/spec_rules.ML"; |
wenzelm@31436 | 240 |
use "Isar/specification.ML"; |
wenzelm@35626 | 241 |
use "Isar/typedecl.ML"; |
wenzelm@31436 | 242 |
|
wenzelm@31436 | 243 |
(*toplevel transactions*) |
wenzelm@38212 | 244 |
use "Thy/thy_load.ML"; |
wenzelm@31436 | 245 |
use "Isar/proof_node.ML"; |
wenzelm@31436 | 246 |
use "Isar/toplevel.ML"; |
wenzelm@31436 | 247 |
|
wenzelm@38569 | 248 |
(*theory documents*) |
wenzelm@40996 | 249 |
use "System/isabelle_system.ML"; |
wenzelm@38212 | 250 |
use "Thy/present.ML"; |
wenzelm@31436 | 251 |
use "Thy/term_style.ML"; |
wenzelm@31436 | 252 |
use "Thy/thy_output.ML"; |
wenzelm@31436 | 253 |
use "Thy/thy_syntax.ML"; |
wenzelm@31436 | 254 |
use "Isar/outer_syntax.ML"; |
wenzelm@38677 | 255 |
use "PIDE/document.ML"; |
wenzelm@31436 | 256 |
use "Thy/thy_info.ML"; |
wenzelm@31436 | 257 |
|
wenzelm@31436 | 258 |
(*theory and proof operations*) |
wenzelm@31436 | 259 |
use "Isar/rule_insts.ML"; |
wenzelm@31436 | 260 |
use "Thy/thm_deps.ML"; |
wenzelm@31436 | 261 |
use "Isar/isar_cmd.ML"; |
wenzelm@31436 | 262 |
use "Isar/isar_syn.ML"; |
wenzelm@31436 | 263 |
|
wenzelm@20207 | 264 |
use "subgoal.ML"; |
wenzelm@5834 | 265 |
|
berghofe@13402 | 266 |
use "Proof/extraction.ML"; |
berghofe@11511 | 267 |
|
wenzelm@31436 | 268 |
|
wenzelm@31436 | 269 |
(* Isabelle/Isar system *) |
wenzelm@31436 | 270 |
|
wenzelm@30174 | 271 |
use "System/session.ML"; |
wenzelm@38658 | 272 |
use "System/isabelle_process.ML"; |
wenzelm@38801 | 273 |
use "PIDE/isar_document.ML"; |
wenzelm@30174 | 274 |
use "System/isar.ML"; |
wenzelm@30174 | 275 |
|
wenzelm@31436 | 276 |
|
wenzelm@31436 | 277 |
(* miscellaneous tools and packages for Pure Isabelle *) |
wenzelm@31436 | 278 |
|
wenzelm@31436 | 279 |
use "Tools/named_thms.ML"; |
wenzelm@31436 | 280 |
|
wenzelm@31436 | 281 |
use "Tools/xml_syntax.ML"; |
wenzelm@31436 | 282 |
|
wenzelm@31436 | 283 |
use "Tools/find_theorems.ML"; |
wenzelm@31436 | 284 |
use "Tools/find_consts.ML"; |
wenzelm@17467 | 285 |
|
berghofe@24455 | 286 |
use "codegen.ML"; |
berghofe@24455 | 287 |
|
wenzelm@31436 | 288 |
|
wenzelm@31436 | 289 |
(* configuration for Proof General *) |
wenzelm@31436 | 290 |
|
wenzelm@31436 | 291 |
use "ProofGeneral/pgip_types.ML"; |
wenzelm@31436 | 292 |
use "ProofGeneral/pgml.ML"; |
wenzelm@31436 | 293 |
use "ProofGeneral/pgip_markup.ML"; |
wenzelm@31436 | 294 |
use "ProofGeneral/pgip_input.ML"; |
wenzelm@31436 | 295 |
use "ProofGeneral/pgip_output.ML"; |
wenzelm@31436 | 296 |
use "ProofGeneral/pgip.ML"; |
wenzelm@31436 | 297 |
|
wenzelm@31436 | 298 |
use "ProofGeneral/pgip_isabelle.ML"; |
wenzelm@31436 | 299 |
|
wenzelm@31436 | 300 |
use "ProofGeneral/preferences.ML"; |
wenzelm@31436 | 301 |
|
wenzelm@31436 | 302 |
use "ProofGeneral/pgip_parser.ML"; |
wenzelm@31436 | 303 |
|
wenzelm@31436 | 304 |
use "ProofGeneral/pgip_tests.ML"; |
wenzelm@31436 | 305 |
|
wenzelm@31436 | 306 |
use "ProofGeneral/proof_general_pgip.ML"; |
wenzelm@31436 | 307 |
use "ProofGeneral/proof_general_emacs.ML"; |
wenzelm@31436 | 308 |
|
obua@16781 | 309 |
|
wenzelm@23825 | 310 |
use "pure_setup.ML"; |
wenzelm@30643 | 311 |