0

1 
(* Title: ROOT


2 
ID: $Id$


3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory


4 
Copyright 1993 University of Cambridge


5 


6 
Root file for pure Isabelle: all modules in proper order for loading


7 
Loads pure Isabelle into an empty database.


8 


9 
To build system, use Makefile (Poly/ML) or Makefile.NJ (New Jersey ML)


10 


11 
TO DO:


12 
instantiation of theorems can lead to inconsistent sorting of type vars if


13 
'a::S is already present and 'a::T is introduced.


14 
*)


15 


16 
val banner = "Pure Isabelle";


17 
val version = "February 93";


18 


19 
print_depth 1;


20 


21 
use "library.ML";


22 
use "term.ML";


23 
use "symtab.ML";


24 


25 
(*Used for building the parser generator*)


26 
structure Symtab = SymtabFun();


27 
cd "Syntax";


28 
use "ROOT.ML";


29 
cd "..";


30 


31 
(* Theory parser *)


32 
cd "Thy";


33 
use "ROOT.ML";


34 
cd "..";


35 


36 
print_depth 1;


37 
use "type.ML";


38 
use "sign.ML";


39 
use "sequence.ML";


40 
use "envir.ML";


41 
use "pattern.ML";


42 
use "unify.ML";


43 
use "net.ML";


44 
use "logic.ML";


45 
use "thm.ML";


46 
use "drule.ML";


47 
use "tctical.ML";


48 
use "tactic.ML";


49 
use "goals.ML";


50 


51 
(*Will be visible to all objectlogics.*)


52 
structure Type = TypeFun(structure Symtab=Symtab and Syntax=Syntax);


53 
structure Sign = SignFun(structure Type=Type and Syntax=Syntax);


54 
structure Sequence = SequenceFun();


55 
structure Envir = EnvirFun();


56 
structure Pattern = PatternFun(structure Sign=Sign and Envir=Envir);


57 
structure Unify = UnifyFun(structure Sign=Sign and Envir=Envir


58 
and Sequence=Sequence and Pattern=Pattern);


59 
structure Net = NetFun();


60 
structure Logic = LogicFun(structure Unify=Unify and Net=Net);


61 
structure Thm = ThmFun(structure Logic=Logic and Unify=Unify and Net=Net


62 
and Pattern=Pattern);


63 
structure Drule = DruleFun(structure Logic=Logic and Thm=Thm);


64 
structure Tactical = TacticalFun(structure Logic=Logic and Drule=Drule);


65 
structure Tactic = TacticFun(structure Logic=Logic and Drule=Drule


66 
and Tactical=Tactical and Net=Net);


67 
structure Goals = GoalsFun(structure Logic=Logic and Drule=Drule


68 
and Tactic=Tactic and Pattern=Pattern);


69 
open Basic_Syntax Thm Drule Tactical Tactic Goals;


70 


71 
structure Pure = struct val thy = pure_thy end;
