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 |
(* Theory parser *)
|
|
32 |
cd "Thy";
|
|
33 |
use "ROOT.ML";
|
|
34 |
cd "..";
|
|
35 |
|
|
36 |
print_depth 1;
|
|
37 |
use "type.ML";
|
|
38 |
use "sign.ML";
|
|
39 |
use "sequence.ML";
|
|
40 |
use "envir.ML";
|
|
41 |
use "pattern.ML";
|
|
42 |
use "unify.ML";
|
|
43 |
use "net.ML";
|
|
44 |
use "logic.ML";
|
|
45 |
use "thm.ML";
|
|
46 |
use "drule.ML";
|
|
47 |
use "tctical.ML";
|
|
48 |
use "tactic.ML";
|
|
49 |
use "goals.ML";
|
|
50 |
|
|
51 |
(*Will be visible to all object-logics.*)
|
|
52 |
structure Type = TypeFun(structure Symtab=Symtab and Syntax=Syntax);
|
|
53 |
structure Sign = SignFun(structure Type=Type and Syntax=Syntax);
|
|
54 |
structure Sequence = SequenceFun();
|
|
55 |
structure Envir = EnvirFun();
|
|
56 |
structure Pattern = PatternFun(structure Sign=Sign and Envir=Envir);
|
|
57 |
structure Unify = UnifyFun(structure Sign=Sign and Envir=Envir
|
|
58 |
and Sequence=Sequence and Pattern=Pattern);
|
|
59 |
structure Net = NetFun();
|
|
60 |
structure Logic = LogicFun(structure Unify=Unify and Net=Net);
|
|
61 |
structure Thm = ThmFun(structure Logic=Logic and Unify=Unify and Net=Net
|
|
62 |
and Pattern=Pattern);
|
|
63 |
structure Drule = DruleFun(structure Logic=Logic and Thm=Thm);
|
|
64 |
structure Tactical = TacticalFun(structure Logic=Logic and Drule=Drule);
|
|
65 |
structure Tactic = TacticFun(structure Logic=Logic and Drule=Drule
|
|
66 |
and Tactical=Tactical and Net=Net);
|
|
67 |
structure Goals = GoalsFun(structure Logic=Logic and Drule=Drule
|
|
68 |
and Tactic=Tactic and Pattern=Pattern);
|
|
69 |
open Basic_Syntax Thm Drule Tactical Tactic Goals;
|
|
70 |
|
|
71 |
structure Pure = struct val thy = pure_thy end;
|