src/Pure/ROOT.ML
changeset 0 a5a9c433f639
child 2 c67f44be880f
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/ROOT.ML	Thu Sep 16 12:20:38 1993 +0200
     1.3 @@ -0,0 +1,71 @@
     1.4 +(*  Title: 	ROOT
     1.5 +    ID:         $Id$
     1.6 +    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 +    Copyright   1993  University of Cambridge
     1.8 +
     1.9 +Root file for pure Isabelle: all modules in proper order for loading
    1.10 +Loads pure Isabelle into an empty database.
    1.11 +
    1.12 +To build system, use Makefile (Poly/ML) or Makefile.NJ (New Jersey ML)
    1.13 +
    1.14 +TO DO: 
    1.15 +instantiation of theorems can lead to inconsistent sorting of type vars if
    1.16 +'a::S is already present and 'a::T is introduced. 
    1.17 +*)
    1.18 +
    1.19 +val banner = "Pure Isabelle";
    1.20 +val version = "February 93";
    1.21 +
    1.22 +print_depth 1;
    1.23 +
    1.24 +use "library.ML";
    1.25 +use "term.ML";
    1.26 +use "symtab.ML";
    1.27 +
    1.28 +(*Used for building the parser generator*)
    1.29 +structure Symtab = SymtabFun();
    1.30 +cd "Syntax";
    1.31 +use "ROOT.ML";
    1.32 +cd "..";
    1.33 +
    1.34 +(* Theory parser *)
    1.35 +cd "Thy";
    1.36 +use "ROOT.ML";
    1.37 +cd "..";
    1.38 +
    1.39 +print_depth 1;
    1.40 +use "type.ML";
    1.41 +use "sign.ML";
    1.42 +use "sequence.ML";
    1.43 +use "envir.ML";
    1.44 +use "pattern.ML";
    1.45 +use "unify.ML";
    1.46 +use "net.ML";
    1.47 +use "logic.ML";
    1.48 +use "thm.ML";
    1.49 +use "drule.ML";
    1.50 +use "tctical.ML";
    1.51 +use "tactic.ML";
    1.52 +use "goals.ML";
    1.53 +
    1.54 +(*Will be visible to all object-logics.*)
    1.55 +structure Type = TypeFun(structure Symtab=Symtab and Syntax=Syntax);
    1.56 +structure Sign = SignFun(structure Type=Type and Syntax=Syntax);
    1.57 +structure Sequence = SequenceFun();
    1.58 +structure Envir = EnvirFun();
    1.59 +structure Pattern = PatternFun(structure Sign=Sign and Envir=Envir);
    1.60 +structure Unify = UnifyFun(structure Sign=Sign and Envir=Envir
    1.61 +			   and Sequence=Sequence and Pattern=Pattern);
    1.62 +structure Net = NetFun();
    1.63 +structure Logic = LogicFun(structure Unify=Unify and Net=Net);
    1.64 +structure Thm = ThmFun(structure Logic=Logic and Unify=Unify and Net=Net
    1.65 +                             and Pattern=Pattern); 
    1.66 +structure Drule = DruleFun(structure Logic=Logic and Thm=Thm);
    1.67 +structure Tactical = TacticalFun(structure Logic=Logic and Drule=Drule);
    1.68 +structure Tactic = TacticFun(structure Logic=Logic and Drule=Drule 
    1.69 +			     and Tactical=Tactical and Net=Net);
    1.70 +structure Goals = GoalsFun(structure Logic=Logic and Drule=Drule
    1.71 +			   and Tactic=Tactic and Pattern=Pattern);
    1.72 +open Basic_Syntax Thm Drule Tactical Tactic Goals;
    1.73 +
    1.74 +structure Pure = struct val thy = pure_thy end;