author | wenzelm |
Tue, 17 Mar 2009 14:12:06 +0100 | |
changeset 30561 | e5987a7ac5df |
parent 30174 | eabece26b89b |
child 30643 | fe40d740d7c1 |
permissions | -rw-r--r-- |
wenzelm@19 | 1 |
(* Title: Pure/ROOT.ML |
clasohm@0 | 2 |
|
wenzelm@16842 | 3 |
Pure Isabelle. |
clasohm@0 | 4 |
*) |
clasohm@0 | 5 |
|
wenzelm@26109 | 6 |
structure Distribution = (*filled-in by makedist*) |
wenzelm@26109 | 7 |
struct |
wenzelm@26109 | 8 |
val version = "Isabelle repository version"; |
wenzelm@27642 | 9 |
val is_official = false; |
wenzelm@27642 | 10 |
val changelog = ""; |
wenzelm@26109 | 11 |
end; |
wenzelm@11835 | 12 |
|
wenzelm@23825 | 13 |
(*if true then some tools will OMIT some proofs*) |
wenzelm@23825 | 14 |
val quick_and_dirty = ref false; |
wenzelm@23825 | 15 |
|
wenzelm@12248 | 16 |
print_depth 10; |
clasohm@0 | 17 |
|
wenzelm@5017 | 18 |
(*basic tools*) |
wenzelm@21396 | 19 |
use "General/basics.ML"; |
clasohm@0 | 20 |
use "library.ML"; |
wenzelm@22592 | 21 |
|
wenzelm@5017 | 22 |
cd "General"; use "ROOT.ML"; cd ".."; |
wenzelm@28200 | 23 |
cd "Concurrent"; use "ROOT.ML"; cd ".."; |
wenzelm@28120 | 24 |
|
wenzelm@14781 | 25 |
(*fundamental structures*) |
wenzelm@20075 | 26 |
use "name.ML"; |
clasohm@0 | 27 |
use "term.ML"; |
wenzelm@29269 | 28 |
use "term_ord.ML"; |
wenzelm@20507 | 29 |
use "term_subst.ML"; |
wenzelm@29263 | 30 |
use "old_term.ML"; |
wenzelm@24257 | 31 |
use "logic.ML"; |
wenzelm@14823 | 32 |
use "General/pretty.ML"; |
wenzelm@28404 | 33 |
use "context.ML"; |
wenzelm@28404 | 34 |
use "context_position.ML"; |
wenzelm@24235 | 35 |
use "Syntax/lexicon.ML"; |
wenzelm@24235 | 36 |
use "Syntax/simple_syntax.ML"; |
wenzelm@14781 | 37 |
use "sorts.ML"; |
wenzelm@14781 | 38 |
use "type.ML"; |
wenzelm@24113 | 39 |
use "config.ML"; |
wenzelm@19 | 40 |
|
wenzelm@4949 | 41 |
(*inner syntax module*) |
wenzelm@22679 | 42 |
use "Syntax/ast.ML"; |
wenzelm@22679 | 43 |
use "Syntax/syn_ext.ML"; |
wenzelm@22679 | 44 |
use "Syntax/parser.ML"; |
wenzelm@22679 | 45 |
use "Syntax/type_ext.ML"; |
wenzelm@22679 | 46 |
use "Syntax/syn_trans.ML"; |
wenzelm@22679 | 47 |
use "Syntax/mixfix.ML"; |
wenzelm@22679 | 48 |
use "Syntax/printer.ML"; |
wenzelm@22679 | 49 |
use "Syntax/syntax.ML"; |
wenzelm@22679 | 50 |
|
wenzelm@27262 | 51 |
use "type_infer.ML"; |
wenzelm@24574 | 52 |
use "ML/ml_syntax.ML"; |
clasohm@0 | 53 |
|
wenzelm@15825 | 54 |
(*core of tactical proof system*) |
wenzelm@30561 | 55 |
use "net.ML"; |
wenzelm@30561 | 56 |
use "item_net.ML"; |
wenzelm@18934 | 57 |
use "envir.ML"; |
wenzelm@18059 | 58 |
use "consts.ML"; |
wenzelm@24257 | 59 |
use "primitive_defs.ML"; |
haftmann@27546 | 60 |
use "defs.ML"; |
clasohm@0 | 61 |
use "sign.ML"; |
clasohm@0 | 62 |
use "pattern.ML"; |
clasohm@0 | 63 |
use "unify.ML"; |
paulson@1528 | 64 |
use "theory.ML"; |
wenzelm@24664 | 65 |
use "interpretation.ML"; |
berghofe@11511 | 66 |
use "proofterm.ML"; |
clasohm@0 | 67 |
use "thm.ML"; |
wenzelm@22361 | 68 |
use "more_thm.ML"; |
wenzelm@26279 | 69 |
use "facts.ML"; |
wenzelm@3986 | 70 |
use "pure_thy.ML"; |
wenzelm@19589 | 71 |
use "display.ML"; |
clasohm@0 | 72 |
use "drule.ML"; |
wenzelm@22233 | 73 |
use "morphism.ML"; |
wenzelm@19898 | 74 |
use "variable.ML"; |
wenzelm@24833 | 75 |
use "conv.ML"; |
clasohm@0 | 76 |
use "tctical.ML"; |
paulson@1582 | 77 |
use "search.ML"; |
wenzelm@21708 | 78 |
use "tactic.ML"; |
skalberg@15006 | 79 |
use "meta_simplifier.ML"; |
wenzelm@19417 | 80 |
use "conjunction.ML"; |
wenzelm@20225 | 81 |
use "assumption.ML"; |
wenzelm@17963 | 82 |
use "goal.ML"; |
wenzelm@24963 | 83 |
use "axclass.ML"; |
clasohm@0 | 84 |
|
wenzelm@30174 | 85 |
(*main Isar stuff*) |
wenzelm@6178 | 86 |
cd "Isar"; use "ROOT.ML"; cd ".."; |
wenzelm@20207 | 87 |
use "subgoal.ML"; |
wenzelm@5834 | 88 |
|
berghofe@13402 | 89 |
use "Proof/extraction.ML"; |
berghofe@11511 | 90 |
|
wenzelm@30174 | 91 |
(*Isabelle/Isar system*) |
wenzelm@30174 | 92 |
use "System/session.ML"; |
wenzelm@30174 | 93 |
use "System/isar.ML"; |
wenzelm@30174 | 94 |
use "System/isabelle_process.ML"; |
wenzelm@30174 | 95 |
|
wenzelm@30174 | 96 |
(*additional tools*) |
wenzelm@17467 | 97 |
cd "Tools"; use "ROOT.ML"; cd ".."; |
wenzelm@17467 | 98 |
|
berghofe@24455 | 99 |
use "codegen.ML"; |
berghofe@24455 | 100 |
|
wenzelm@12778 | 101 |
(*configuration for Proof General*) |
wenzelm@21941 | 102 |
cd "ProofGeneral"; use "ROOT.ML"; cd ".."; |
obua@16781 | 103 |
|
wenzelm@23825 | 104 |
use "pure_setup.ML"; |