author  lcp 
Tue, 21 Jun 1994 17:20:34 +0200  
changeset 435  ca5356bd315a 
parent 403  4c66b1577753 
child 607  72fc777dbda0 
permissions  rwrr 
19  1 
(* Title: Pure/ROOT.ML 
0  2 
ID: $Id$ 
19  3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
0  4 
Copyright 1993 University of Cambridge 
5 

19  6 
Root file for Pure Isabelle: all modules in proper order for loading. 
7 
Loads pure Isabelle into an empty database (see also Makefile). 

0  8 

19  9 
TO DO: 
0  10 
instantiation of theorems can lead to inconsistent sorting of type vars if 
19  11 
'a::S is already present and 'a::T is introduced. 
0  12 
*) 
13 

14 
val banner = "Pure Isabelle"; 

83  15 
val version = "October 93"; 
0  16 

17 
print_depth 1; 

18 

19 
use "library.ML"; 

20 
use "term.ML"; 

21 
use "symtab.ML"; 

22 

23 
structure Symtab = SymtabFun(); 

19  24 

25 
(*Syntax module*) 

0  26 
cd "Syntax"; 
27 
use "ROOT.ML"; 

28 
cd ".."; 

29 

30 
use "type.ML"; 

31 
use "sign.ML"; 

32 
use "sequence.ML"; 

33 
use "envir.ML"; 

34 
use "pattern.ML"; 

35 
use "unify.ML"; 

36 
use "net.ML"; 

37 
use "logic.ML"; 

38 
use "thm.ML"; 

39 
use "drule.ML"; 

40 
use "tctical.ML"; 

41 
use "tactic.ML"; 

42 
use "goals.ML"; 

403  43 
use "axclass.ML"; 
0  44 

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

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

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

48 
structure Sequence = SequenceFun(); 

49 
structure Envir = EnvirFun(); 

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

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

19  52 
and Sequence=Sequence and Pattern=Pattern); 
0  53 
structure Net = NetFun(); 
54 
structure Logic = LogicFun(structure Unify=Unify and Net=Net); 

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

19  56 
and Pattern=Pattern); 
0  57 
structure Drule = DruleFun(structure Logic=Logic and Thm=Thm); 
58 
structure Tactical = TacticalFun(structure Logic=Logic and Drule=Drule); 

19  59 
structure Tactic = TacticFun(structure Logic=Logic and Drule=Drule 
60 
and Tactical=Tactical and Net=Net); 

0  61 
structure Goals = GoalsFun(structure Logic=Logic and Drule=Drule 
19  62 
and Tactic=Tactic and Pattern=Pattern); 
403  63 
structure AxClass = AxClassFun(structure Logic = Logic 
64 
and Goals = Goals and Tactic = Tactic); 

65 
open BasicSyntax Thm Drule Tactical Tactic Goals AxClass; 

0  66 

67 
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

68 

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

70 

73
075db6ac7f2f
delete_file now has type string > unit in both NJ and POLY,
clasohm
parents:
19
diff
changeset

71 

075db6ac7f2f
delete_file now has type string > unit in both NJ and POLY,
clasohm
parents:
19
diff
changeset

72 

075db6ac7f2f
delete_file now has type string > unit in both NJ and POLY,
clasohm
parents:
19
diff
changeset

73 
(*Theory parser 
075db6ac7f2f
delete_file now has type string > unit in both NJ and POLY,
clasohm
parents:
19
diff
changeset

74 
(The new Thy/read.ML needs Thm so this has to be done AFTER Thm is 
075db6ac7f2f
delete_file now has type string > unit in both NJ and POLY,
clasohm
parents:
19
diff
changeset

75 
created.) *) 
075db6ac7f2f
delete_file now has type string > unit in both NJ and POLY,
clasohm
parents:
19
diff
changeset

76 
cd "Thy"; 
075db6ac7f2f
delete_file now has type string > unit in both NJ and POLY,
clasohm
parents:
19
diff
changeset

77 
use "ROOT.ML"; 
075db6ac7f2f
delete_file now has type string > unit in both NJ and POLY,
clasohm
parents:
19
diff
changeset

78 
cd ".."; 
075db6ac7f2f
delete_file now has type string > unit in both NJ and POLY,
clasohm
parents:
19
diff
changeset

79 