author  clasohm 
Thu, 16 Sep 1993 16:25:32 +0200  
changeset 2  c67f44be880f 
parent 0  a5a9c433f639 
child 19  929ad32d63fc 
permissions  rwrr 
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 
print_depth 1; 

32 
use "type.ML"; 

33 
use "sign.ML"; 

34 
use "sequence.ML"; 

35 
use "envir.ML"; 

36 
use "pattern.ML"; 

37 
use "unify.ML"; 

38 
use "net.ML"; 

39 
use "logic.ML"; 

40 
use "thm.ML"; 

41 
use "drule.ML"; 

42 
use "tctical.ML"; 

43 
use "tactic.ML"; 

44 
use "goals.ML"; 

45 

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

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

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

49 
structure Sequence = SequenceFun(); 

50 
structure Envir = EnvirFun(); 

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

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

53 
and Sequence=Sequence and Pattern=Pattern); 

54 
structure Net = NetFun(); 

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

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

57 
and Pattern=Pattern); 

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

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

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

61 
and Tactical=Tactical and Net=Net); 

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

63 
and Tactic=Tactic and Pattern=Pattern); 

64 
open Basic_Syntax Thm Drule Tactical Tactic Goals; 

65 

66 
structure Pure = struct val thy = pure_thy end; 

2
c67f44be880f
moved use of Thy/ROOT.ML to end of file because Thy/read.ML needs Thm
clasohm
parents:
0
diff
changeset

67 

c67f44be880f
moved use of Thy/ROOT.ML to end of file because Thy/read.ML needs Thm
clasohm
parents:
0
diff
changeset

68 
(* Theory parser *) 
c67f44be880f
moved use of Thy/ROOT.ML to end of file because Thy/read.ML needs Thm
clasohm
parents:
0
diff
changeset

69 
cd "Thy"; 
c67f44be880f
moved use of Thy/ROOT.ML to end of file because Thy/read.ML needs Thm
clasohm
parents:
0
diff
changeset

70 
use "ROOT.ML"; 
c67f44be880f
moved use of Thy/ROOT.ML to end of file because Thy/read.ML needs Thm
clasohm
parents:
0
diff
changeset

71 
cd ".."; 
c67f44be880f
moved use of Thy/ROOT.ML to end of file because Thy/read.ML needs Thm
clasohm
parents:
0
diff
changeset

72 