author | wenzelm |
Wed, 12 Oct 1994 16:29:10 +0100 | |
changeset 635 | 034fda1c4873 |
parent 618 | 97b715e65f70 |
child 913 | 8aaa8c5a567e |
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"; |
|
607 | 15 |
val version = "Isabelle-94: September 94"; |
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 object-logics.*) |
|
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); |
618 | 63 |
structure AxClass = AxClassFun(structure Logic = Logic |
403 | 64 |
and Goals = Goals and Tactic = Tactic); |
635 | 65 |
open BasicSyntax Thm Drule Tactical Tactic Goals; |
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 |
|
618 | 69 |
(*Theory parser and loader*) |
73
075db6ac7f2f
delete_file now has type string -> unit in both NJ and POLY,
clasohm
parents:
19
diff
changeset
|
70 |
cd "Thy"; |
075db6ac7f2f
delete_file now has type string -> unit in both NJ and POLY,
clasohm
parents:
19
diff
changeset
|
71 |
use "ROOT.ML"; |
075db6ac7f2f
delete_file now has type string -> unit in both NJ and POLY,
clasohm
parents:
19
diff
changeset
|
72 |
cd ".."; |
075db6ac7f2f
delete_file now has type string -> unit in both NJ and POLY,
clasohm
parents:
19
diff
changeset
|
73 |
|
618 | 74 |
use "install_pp.ML"; |
75 |
fun init_database () = (init_thy_reader (); init_pps ()); |
|
76 |