author | lcp |
Thu, 28 Oct 1993 11:28:36 +0100 | |
changeset 83 | de9316670e89 |
parent 73 | 075db6ac7f2f |
child 403 | 4c66b1577753 |
permissions | -rw-r--r-- |
wenzelm@19 | 1 |
(* Title: Pure/ROOT.ML |
clasohm@0 | 2 |
ID: $Id$ |
wenzelm@19 | 3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
clasohm@0 | 4 |
Copyright 1993 University of Cambridge |
clasohm@0 | 5 |
|
wenzelm@19 | 6 |
Root file for Pure Isabelle: all modules in proper order for loading. |
wenzelm@19 | 7 |
Loads pure Isabelle into an empty database (see also Makefile). |
clasohm@0 | 8 |
|
wenzelm@19 | 9 |
TO DO: |
clasohm@0 | 10 |
instantiation of theorems can lead to inconsistent sorting of type vars if |
wenzelm@19 | 11 |
'a::S is already present and 'a::T is introduced. |
clasohm@0 | 12 |
*) |
clasohm@0 | 13 |
|
clasohm@0 | 14 |
val banner = "Pure Isabelle"; |
lcp@83 | 15 |
val version = "October 93"; |
clasohm@0 | 16 |
|
clasohm@0 | 17 |
print_depth 1; |
clasohm@0 | 18 |
|
clasohm@0 | 19 |
use "library.ML"; |
clasohm@0 | 20 |
use "term.ML"; |
clasohm@0 | 21 |
use "symtab.ML"; |
clasohm@0 | 22 |
|
clasohm@0 | 23 |
structure Symtab = SymtabFun(); |
wenzelm@19 | 24 |
|
wenzelm@19 | 25 |
(*Syntax module*) |
clasohm@0 | 26 |
cd "Syntax"; |
clasohm@0 | 27 |
use "ROOT.ML"; |
clasohm@0 | 28 |
cd ".."; |
clasohm@0 | 29 |
|
clasohm@0 | 30 |
use "type.ML"; |
clasohm@0 | 31 |
use "sign.ML"; |
clasohm@0 | 32 |
use "sequence.ML"; |
clasohm@0 | 33 |
use "envir.ML"; |
clasohm@0 | 34 |
use "pattern.ML"; |
clasohm@0 | 35 |
use "unify.ML"; |
clasohm@0 | 36 |
use "net.ML"; |
clasohm@0 | 37 |
use "logic.ML"; |
clasohm@0 | 38 |
use "thm.ML"; |
clasohm@0 | 39 |
use "drule.ML"; |
clasohm@0 | 40 |
use "tctical.ML"; |
clasohm@0 | 41 |
use "tactic.ML"; |
clasohm@0 | 42 |
use "goals.ML"; |
clasohm@0 | 43 |
|
clasohm@0 | 44 |
(*Will be visible to all object-logics.*) |
clasohm@0 | 45 |
structure Type = TypeFun(structure Symtab=Symtab and Syntax=Syntax); |
clasohm@0 | 46 |
structure Sign = SignFun(structure Type=Type and Syntax=Syntax); |
clasohm@0 | 47 |
structure Sequence = SequenceFun(); |
clasohm@0 | 48 |
structure Envir = EnvirFun(); |
clasohm@0 | 49 |
structure Pattern = PatternFun(structure Sign=Sign and Envir=Envir); |
clasohm@0 | 50 |
structure Unify = UnifyFun(structure Sign=Sign and Envir=Envir |
wenzelm@19 | 51 |
and Sequence=Sequence and Pattern=Pattern); |
clasohm@0 | 52 |
structure Net = NetFun(); |
clasohm@0 | 53 |
structure Logic = LogicFun(structure Unify=Unify and Net=Net); |
clasohm@0 | 54 |
structure Thm = ThmFun(structure Logic=Logic and Unify=Unify and Net=Net |
wenzelm@19 | 55 |
and Pattern=Pattern); |
clasohm@0 | 56 |
structure Drule = DruleFun(structure Logic=Logic and Thm=Thm); |
clasohm@0 | 57 |
structure Tactical = TacticalFun(structure Logic=Logic and Drule=Drule); |
wenzelm@19 | 58 |
structure Tactic = TacticFun(structure Logic=Logic and Drule=Drule |
wenzelm@19 | 59 |
and Tactical=Tactical and Net=Net); |
clasohm@0 | 60 |
structure Goals = GoalsFun(structure Logic=Logic and Drule=Drule |
wenzelm@19 | 61 |
and Tactic=Tactic and Pattern=Pattern); |
wenzelm@19 | 62 |
open BasicSyntax Thm Drule Tactical Tactic Goals; |
clasohm@0 | 63 |
|
clasohm@0 | 64 |
structure Pure = struct val thy = pure_thy end; |
clasohm@2 | 65 |
|
wenzelm@19 | 66 |
use "install_pp.ML"; |
clasohm@2 | 67 |
|
clasohm@73 | 68 |
|
clasohm@73 | 69 |
|
clasohm@73 | 70 |
(*Theory parser |
clasohm@73 | 71 |
(The new Thy/read.ML needs Thm so this has to be done AFTER Thm is |
clasohm@73 | 72 |
created.) *) |
clasohm@73 | 73 |
cd "Thy"; |
clasohm@73 | 74 |
use "ROOT.ML"; |
clasohm@73 | 75 |
cd ".."; |
clasohm@73 | 76 |