author  paulson 
Thu, 21 Mar 1996 11:04:36 +0100  
changeset 1595  b9984b1dbc4c 
parent 1582  97a305db0c9e 
child 1864  9ac4c2240d89 
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"; 

1443  15 
val version = "Isabelle94 revision 5: January 96"; 
0  16 

17 
print_depth 1; 

18 

19 
use "library.ML"; 

1411  20 
use "symtab.ML"; 
0  21 
use "term.ML"; 
19  22 

23 
(*Syntax module*) 

0  24 
cd "Syntax"; 
25 
use "ROOT.ML"; 

26 
cd ".."; 

27 

28 
use "type.ML"; 

29 
use "sign.ML"; 

30 
use "sequence.ML"; 

31 
use "envir.ML"; 

32 
use "pattern.ML"; 

33 
use "unify.ML"; 

34 
use "net.ML"; 

35 
use "logic.ML"; 

1528  36 
use "theory.ML"; 
0  37 
use "thm.ML"; 
1595  38 
use "deriv.ML"; 
39 
use "display.ML"; 

0  40 
use "drule.ML"; 
41 
use "tctical.ML"; 

1582  42 
use "search.ML"; 
0  43 
use "tactic.ML"; 
44 
use "goals.ML"; 

403  45 
use "axclass.ML"; 
0  46 

1528  47 
structure Pure = struct val thy = Theory.pure_thy end; 
48 
structure CPure = struct val thy = Theory.cpure_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

49 

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

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

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

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

54 

618  55 
use "install_pp.ML"; 
56 
fun init_database () = (init_thy_reader (); init_pps ()); 

57 