author | wenzelm |
Thu, 04 Jun 2009 18:00:47 +0200 | |
changeset 31436 | 9858f32f9569 |
parent 31369 | ba5b7749fa61 |
child 31476 | c5d2899b6de9 |
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@26109 | 5 |
val version = "Isabelle 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@23825 | 11 |
val quick_and_dirty = 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@31436 | 24 |
use "General/properties.ML"; |
wenzelm@31436 | 25 |
use "General/markup.ML"; |
wenzelm@31436 | 26 |
use "General/scan.ML"; |
wenzelm@31436 | 27 |
use "General/source.ML"; |
wenzelm@31436 | 28 |
use "General/symbol.ML"; |
wenzelm@31436 | 29 |
use "General/seq.ML"; |
wenzelm@31436 | 30 |
use "General/position.ML"; |
wenzelm@31436 | 31 |
use "General/symbol_pos.ML"; |
wenzelm@31436 | 32 |
use "General/antiquote.ML"; |
wenzelm@31436 | 33 |
use "ML/ml_lex.ML"; |
wenzelm@31436 | 34 |
use "ML/ml_parse.ML"; |
wenzelm@31436 | 35 |
use "General/secure.ML"; |
wenzelm@31436 | 36 |
(*----- basic ML bootstrap finished -----*) |
wenzelm@31436 | 37 |
use "General/integer.ML"; |
wenzelm@31436 | 38 |
use "General/stack.ML"; |
wenzelm@31436 | 39 |
use "General/queue.ML"; |
wenzelm@31436 | 40 |
use "General/heap.ML"; |
wenzelm@31436 | 41 |
use "General/ord_list.ML"; |
wenzelm@31436 | 42 |
use "General/balanced_tree.ML"; |
wenzelm@31436 | 43 |
use "General/graph.ML"; |
wenzelm@31436 | 44 |
use "General/long_name.ML"; |
wenzelm@31436 | 45 |
use "General/binding.ML"; |
wenzelm@31436 | 46 |
use "General/name_space.ML"; |
wenzelm@31436 | 47 |
use "General/lazy.ML"; |
wenzelm@31436 | 48 |
use "General/path.ML"; |
wenzelm@31436 | 49 |
use "General/url.ML"; |
wenzelm@31436 | 50 |
use "General/buffer.ML"; |
wenzelm@31436 | 51 |
use "General/file.ML"; |
wenzelm@31436 | 52 |
use "General/xml.ML"; |
wenzelm@31436 | 53 |
use "General/yxml.ML"; |
wenzelm@22592 | 54 |
|
wenzelm@28120 | 55 |
|
wenzelm@31436 | 56 |
(* concurrency within the ML runtime *) |
wenzelm@31436 | 57 |
|
wenzelm@31436 | 58 |
use "Concurrent/simple_thread.ML"; |
wenzelm@31436 | 59 |
use "Concurrent/synchronized.ML"; |
wenzelm@31436 | 60 |
use "Concurrent/mailbox.ML"; |
wenzelm@31436 | 61 |
use "Concurrent/task_queue.ML"; |
wenzelm@31436 | 62 |
use "Concurrent/future.ML"; |
wenzelm@31436 | 63 |
use "Concurrent/par_list.ML"; |
wenzelm@31436 | 64 |
if Multithreading.available then () else use "Concurrent/par_list_dummy.ML"; |
wenzelm@31436 | 65 |
|
wenzelm@31436 | 66 |
|
wenzelm@31436 | 67 |
(* fundamental structures *) |
wenzelm@31436 | 68 |
|
wenzelm@20075 | 69 |
use "name.ML"; |
clasohm@0 | 70 |
use "term.ML"; |
wenzelm@29269 | 71 |
use "term_ord.ML"; |
wenzelm@20507 | 72 |
use "term_subst.ML"; |
wenzelm@29263 | 73 |
use "old_term.ML"; |
wenzelm@24257 | 74 |
use "logic.ML"; |
wenzelm@14823 | 75 |
use "General/pretty.ML"; |
wenzelm@28404 | 76 |
use "context.ML"; |
wenzelm@28404 | 77 |
use "context_position.ML"; |
wenzelm@24235 | 78 |
use "Syntax/lexicon.ML"; |
wenzelm@24235 | 79 |
use "Syntax/simple_syntax.ML"; |
wenzelm@14781 | 80 |
use "sorts.ML"; |
wenzelm@14781 | 81 |
use "type.ML"; |
wenzelm@24113 | 82 |
use "config.ML"; |
wenzelm@19 | 83 |
|
wenzelm@31436 | 84 |
|
wenzelm@31436 | 85 |
(* inner syntax *) |
wenzelm@31436 | 86 |
|
wenzelm@22679 | 87 |
use "Syntax/ast.ML"; |
wenzelm@22679 | 88 |
use "Syntax/syn_ext.ML"; |
wenzelm@22679 | 89 |
use "Syntax/parser.ML"; |
wenzelm@22679 | 90 |
use "Syntax/type_ext.ML"; |
wenzelm@22679 | 91 |
use "Syntax/syn_trans.ML"; |
wenzelm@22679 | 92 |
use "Syntax/mixfix.ML"; |
wenzelm@22679 | 93 |
use "Syntax/printer.ML"; |
wenzelm@22679 | 94 |
use "Syntax/syntax.ML"; |
wenzelm@22679 | 95 |
|
wenzelm@27262 | 96 |
use "type_infer.ML"; |
wenzelm@31360 | 97 |
|
wenzelm@31436 | 98 |
|
wenzelm@31436 | 99 |
(* core of tactical proof system *) |
wenzelm@31436 | 100 |
|
wenzelm@30561 | 101 |
use "net.ML"; |
wenzelm@30561 | 102 |
use "item_net.ML"; |
wenzelm@18934 | 103 |
use "envir.ML"; |
wenzelm@18059 | 104 |
use "consts.ML"; |
wenzelm@24257 | 105 |
use "primitive_defs.ML"; |
haftmann@27546 | 106 |
use "defs.ML"; |
clasohm@0 | 107 |
use "sign.ML"; |
clasohm@0 | 108 |
use "pattern.ML"; |
clasohm@0 | 109 |
use "unify.ML"; |
paulson@1528 | 110 |
use "theory.ML"; |
wenzelm@24664 | 111 |
use "interpretation.ML"; |
berghofe@11511 | 112 |
use "proofterm.ML"; |
clasohm@0 | 113 |
use "thm.ML"; |
wenzelm@22361 | 114 |
use "more_thm.ML"; |
wenzelm@26279 | 115 |
use "facts.ML"; |
wenzelm@3986 | 116 |
use "pure_thy.ML"; |
wenzelm@19589 | 117 |
use "display.ML"; |
clasohm@0 | 118 |
use "drule.ML"; |
wenzelm@22233 | 119 |
use "morphism.ML"; |
wenzelm@19898 | 120 |
use "variable.ML"; |
wenzelm@24833 | 121 |
use "conv.ML"; |
clasohm@0 | 122 |
use "tctical.ML"; |
paulson@1582 | 123 |
use "search.ML"; |
wenzelm@21708 | 124 |
use "tactic.ML"; |
skalberg@15006 | 125 |
use "meta_simplifier.ML"; |
wenzelm@19417 | 126 |
use "conjunction.ML"; |
wenzelm@20225 | 127 |
use "assumption.ML"; |
wenzelm@17963 | 128 |
use "goal.ML"; |
wenzelm@24963 | 129 |
use "axclass.ML"; |
clasohm@0 | 130 |
|
wenzelm@31436 | 131 |
|
wenzelm@31436 | 132 |
(* Isar -- Intelligible Semi-Automated Reasoning *) |
wenzelm@31436 | 133 |
|
wenzelm@31436 | 134 |
(*proof context*) |
wenzelm@31436 | 135 |
use "Isar/object_logic.ML"; |
wenzelm@31436 | 136 |
use "Isar/rule_cases.ML"; |
wenzelm@31436 | 137 |
use "Isar/auto_bind.ML"; |
wenzelm@31436 | 138 |
use "Isar/local_syntax.ML"; |
wenzelm@31436 | 139 |
use "Isar/proof_context.ML"; |
wenzelm@31436 | 140 |
use "Isar/local_defs.ML"; |
wenzelm@31436 | 141 |
|
wenzelm@31436 | 142 |
(*proof term operations*) |
wenzelm@31436 | 143 |
use "Proof/reconstruct.ML"; |
wenzelm@31436 | 144 |
use "Proof/proof_syntax.ML"; |
wenzelm@31436 | 145 |
use "Proof/proof_rewrite_rules.ML"; |
wenzelm@31436 | 146 |
use "Proof/proofchecker.ML"; |
wenzelm@31436 | 147 |
|
wenzelm@31436 | 148 |
(*outer syntax*) |
wenzelm@31436 | 149 |
use "Isar/outer_lex.ML"; |
wenzelm@31436 | 150 |
use "Isar/outer_keyword.ML"; |
wenzelm@31436 | 151 |
use "Isar/outer_parse.ML"; |
wenzelm@31436 | 152 |
use "Isar/value_parse.ML"; |
wenzelm@31436 | 153 |
use "Isar/args.ML"; |
wenzelm@31436 | 154 |
|
wenzelm@31436 | 155 |
(*ML support*) |
wenzelm@31436 | 156 |
use "ML/ml_syntax.ML"; |
wenzelm@31436 | 157 |
use "ML/ml_env.ML"; |
wenzelm@31436 | 158 |
if ml_system = "polyml-experimental" |
wenzelm@31436 | 159 |
then use "ML/ml_compiler_polyml-5.3.ML" |
wenzelm@31436 | 160 |
else use "ML/ml_compiler.ML"; |
wenzelm@31436 | 161 |
use "ML/ml_context.ML"; |
wenzelm@31436 | 162 |
|
wenzelm@31436 | 163 |
(*theory sources*) |
wenzelm@31436 | 164 |
use "Thy/thy_header.ML"; |
wenzelm@31436 | 165 |
use "Thy/thy_load.ML"; |
wenzelm@31436 | 166 |
use "Thy/html.ML"; |
wenzelm@31436 | 167 |
use "Thy/latex.ML"; |
wenzelm@31436 | 168 |
use "Thy/present.ML"; |
wenzelm@31436 | 169 |
|
wenzelm@31436 | 170 |
(*basic proof engine*) |
wenzelm@31436 | 171 |
use "Isar/proof_display.ML"; |
wenzelm@31436 | 172 |
use "Isar/attrib.ML"; |
wenzelm@31436 | 173 |
use "ML/ml_antiquote.ML"; |
wenzelm@31436 | 174 |
use "Isar/context_rules.ML"; |
wenzelm@31436 | 175 |
use "Isar/skip_proof.ML"; |
wenzelm@31436 | 176 |
use "Isar/method.ML"; |
wenzelm@31436 | 177 |
use "Isar/proof.ML"; |
wenzelm@31436 | 178 |
use "ML/ml_thms.ML"; |
wenzelm@31436 | 179 |
use "Isar/element.ML"; |
wenzelm@31436 | 180 |
|
wenzelm@31436 | 181 |
(*derived theory and proof elements*) |
wenzelm@31436 | 182 |
use "Isar/calculation.ML"; |
wenzelm@31436 | 183 |
use "Isar/obtain.ML"; |
wenzelm@31436 | 184 |
|
wenzelm@31436 | 185 |
(*local theories and targets*) |
wenzelm@31436 | 186 |
use "Isar/local_theory.ML"; |
wenzelm@31436 | 187 |
use "Isar/overloading.ML"; |
wenzelm@31436 | 188 |
use "Isar/locale.ML"; |
wenzelm@31436 | 189 |
use "Isar/class_target.ML"; |
wenzelm@31436 | 190 |
use "Isar/theory_target.ML"; |
wenzelm@31436 | 191 |
use "Isar/expression.ML"; |
wenzelm@31436 | 192 |
use "Isar/class.ML"; |
wenzelm@31436 | 193 |
|
wenzelm@31436 | 194 |
use "simplifier.ML"; |
wenzelm@31436 | 195 |
|
wenzelm@31436 | 196 |
(*executable theory content*) |
wenzelm@31436 | 197 |
use "Isar/code.ML"; |
wenzelm@31436 | 198 |
|
wenzelm@31436 | 199 |
(*specifications*) |
wenzelm@31436 | 200 |
use "Isar/spec_parse.ML"; |
wenzelm@31436 | 201 |
use "Isar/specification.ML"; |
wenzelm@31436 | 202 |
use "Isar/constdefs.ML"; |
wenzelm@31436 | 203 |
|
wenzelm@31436 | 204 |
(*toplevel transactions*) |
wenzelm@31436 | 205 |
use "Isar/proof_node.ML"; |
wenzelm@31436 | 206 |
use "Isar/toplevel.ML"; |
wenzelm@31436 | 207 |
|
wenzelm@31436 | 208 |
(*theory syntax*) |
wenzelm@31436 | 209 |
use "Thy/term_style.ML"; |
wenzelm@31436 | 210 |
use "Thy/thy_output.ML"; |
wenzelm@31436 | 211 |
use "Thy/thy_syntax.ML"; |
wenzelm@31436 | 212 |
use "old_goals.ML"; |
wenzelm@31436 | 213 |
use "Isar/outer_syntax.ML"; |
wenzelm@31436 | 214 |
use "Thy/thy_info.ML"; |
wenzelm@31436 | 215 |
use "Isar/isar_document.ML"; |
wenzelm@31436 | 216 |
|
wenzelm@31436 | 217 |
(*theory and proof operations*) |
wenzelm@31436 | 218 |
use "Isar/rule_insts.ML"; |
wenzelm@31436 | 219 |
use "Thy/thm_deps.ML"; |
wenzelm@31436 | 220 |
use "Isar/isar_cmd.ML"; |
wenzelm@31436 | 221 |
use "Isar/isar_syn.ML"; |
wenzelm@31436 | 222 |
|
wenzelm@20207 | 223 |
use "subgoal.ML"; |
wenzelm@5834 | 224 |
|
berghofe@13402 | 225 |
use "Proof/extraction.ML"; |
berghofe@11511 | 226 |
|
wenzelm@31436 | 227 |
|
wenzelm@31436 | 228 |
(* Isabelle/Isar system *) |
wenzelm@31436 | 229 |
|
wenzelm@30174 | 230 |
use "System/session.ML"; |
wenzelm@30174 | 231 |
use "System/isar.ML"; |
wenzelm@30174 | 232 |
use "System/isabelle_process.ML"; |
wenzelm@30174 | 233 |
|
wenzelm@31436 | 234 |
|
wenzelm@31436 | 235 |
(* miscellaneous tools and packages for Pure Isabelle *) |
wenzelm@31436 | 236 |
|
wenzelm@31436 | 237 |
use "Tools/named_thms.ML"; |
wenzelm@31436 | 238 |
|
wenzelm@31436 | 239 |
use "Tools/xml_syntax.ML"; |
wenzelm@31436 | 240 |
|
wenzelm@31436 | 241 |
use "Tools/find_theorems.ML"; |
wenzelm@31436 | 242 |
use "Tools/find_consts.ML"; |
wenzelm@17467 | 243 |
|
berghofe@24455 | 244 |
use "codegen.ML"; |
berghofe@24455 | 245 |
|
wenzelm@31436 | 246 |
|
wenzelm@31436 | 247 |
(* configuration for Proof General *) |
wenzelm@31436 | 248 |
|
wenzelm@31436 | 249 |
use "ProofGeneral/pgip_types.ML"; |
wenzelm@31436 | 250 |
use "ProofGeneral/pgml.ML"; |
wenzelm@31436 | 251 |
use "ProofGeneral/pgip_markup.ML"; |
wenzelm@31436 | 252 |
use "ProofGeneral/pgip_input.ML"; |
wenzelm@31436 | 253 |
use "ProofGeneral/pgip_output.ML"; |
wenzelm@31436 | 254 |
use "ProofGeneral/pgip.ML"; |
wenzelm@31436 | 255 |
|
wenzelm@31436 | 256 |
use "ProofGeneral/pgip_isabelle.ML"; |
wenzelm@31436 | 257 |
|
wenzelm@31436 | 258 |
use "ProofGeneral/preferences.ML"; |
wenzelm@31436 | 259 |
|
wenzelm@31436 | 260 |
use "ProofGeneral/pgip_parser.ML"; |
wenzelm@31436 | 261 |
|
wenzelm@31436 | 262 |
use "ProofGeneral/pgip_tests.ML"; |
wenzelm@31436 | 263 |
|
wenzelm@31436 | 264 |
use "ProofGeneral/proof_general_pgip.ML"; |
wenzelm@31436 | 265 |
use "ProofGeneral/proof_general_emacs.ML"; |
wenzelm@31436 | 266 |
|
obua@16781 | 267 |
|
wenzelm@23825 | 268 |
use "pure_setup.ML"; |
wenzelm@30643 | 269 |