author | clasohm |
Fri, 22 Oct 1993 13:39:23 +0100 | |
changeset 73 | 075db6ac7f2f |
parent 19 | 929ad32d63fc |
child 83 | de9316670e89 |
permissions | -rw-r--r-- |
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"; |
|
15 |
val version = "February 93"; |
|
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"; |
|
43 |
||
44 |
(*Will be visible to all object-logics.*) |
|
45 |
structure Type = TypeFun(structure Symtab=Symtab and Syntax=Syntax); |
|
46 |
structure Sign = SignFun(structure Type=Type and Syntax=Syntax); |
|
47 |
structure Sequence = SequenceFun(); |
|
48 |
structure Envir = EnvirFun(); |
|
49 |
structure Pattern = PatternFun(structure Sign=Sign and Envir=Envir); |
|
50 |
structure Unify = UnifyFun(structure Sign=Sign and Envir=Envir |
|
19 | 51 |
and Sequence=Sequence and Pattern=Pattern); |
0 | 52 |
structure Net = NetFun(); |
53 |
structure Logic = LogicFun(structure Unify=Unify and Net=Net); |
|
54 |
structure Thm = ThmFun(structure Logic=Logic and Unify=Unify and Net=Net |
|
19 | 55 |
and Pattern=Pattern); |
0 | 56 |
structure Drule = DruleFun(structure Logic=Logic and Thm=Thm); |
57 |
structure Tactical = TacticalFun(structure Logic=Logic and Drule=Drule); |
|
19 | 58 |
structure Tactic = TacticFun(structure Logic=Logic and Drule=Drule |
59 |
and Tactical=Tactical and Net=Net); |
|
0 | 60 |
structure Goals = GoalsFun(structure Logic=Logic and Drule=Drule |
19 | 61 |
and Tactic=Tactic and Pattern=Pattern); |
62 |
open BasicSyntax Thm Drule Tactical Tactic Goals; |
|
0 | 63 |
|
64 |
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
|
65 |
|
19 | 66 |
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
|
67 |
|
73
075db6ac7f2f
delete_file now has type string -> unit in both NJ and POLY,
clasohm
parents:
19
diff
changeset
|
68 |
|
075db6ac7f2f
delete_file now has type string -> unit in both NJ and POLY,
clasohm
parents:
19
diff
changeset
|
69 |
|
075db6ac7f2f
delete_file now has type string -> unit in both NJ and POLY,
clasohm
parents:
19
diff
changeset
|
70 |
(*Theory parser |
075db6ac7f2f
delete_file now has type string -> unit in both NJ and POLY,
clasohm
parents:
19
diff
changeset
|
71 |
(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
|
72 |
created.) *) |
075db6ac7f2f
delete_file now has type string -> unit in both NJ and POLY,
clasohm
parents:
19
diff
changeset
|
73 |
cd "Thy"; |
075db6ac7f2f
delete_file now has type string -> unit in both NJ and POLY,
clasohm
parents:
19
diff
changeset
|
74 |
use "ROOT.ML"; |
075db6ac7f2f
delete_file now has type string -> unit in both NJ and POLY,
clasohm
parents:
19
diff
changeset
|
75 |
cd ".."; |
075db6ac7f2f
delete_file now has type string -> unit in both NJ and POLY,
clasohm
parents:
19
diff
changeset
|
76 |