author  wenzelm 
Fri, 04 Jun 1999 19:53:27 +0200  
changeset 6771  951d5f5c3c95 
parent 6644  123b215882ae 
child 6783  9cf9c17d9e35 
permissions  rwrr 
5818
962bfe78a297
Isar  Intelligible SemiAutomated Reasoning for Isabelle.
wenzelm
parents:
diff
changeset

1 
(* Title: Pure/Isar/ROOT.ML 
962bfe78a297
Isar  Intelligible SemiAutomated Reasoning for Isabelle.
wenzelm
parents:
diff
changeset

2 
ID: $Id$ 
962bfe78a297
Isar  Intelligible SemiAutomated Reasoning for Isabelle.
wenzelm
parents:
diff
changeset

3 
Author: Markus Wenzel, TU Muenchen 
962bfe78a297
Isar  Intelligible SemiAutomated Reasoning for Isabelle.
wenzelm
parents:
diff
changeset

4 

962bfe78a297
Isar  Intelligible SemiAutomated Reasoning for Isabelle.
wenzelm
parents:
diff
changeset

5 
Isar  Intelligible SemiAutomated Reasoning for Isabelle. 
962bfe78a297
Isar  Intelligible SemiAutomated Reasoning for Isabelle.
wenzelm
parents:
diff
changeset

6 
*) 
962bfe78a297
Isar  Intelligible SemiAutomated Reasoning for Isabelle.
wenzelm
parents:
diff
changeset

7 

962bfe78a297
Isar  Intelligible SemiAutomated Reasoning for Isabelle.
wenzelm
parents:
diff
changeset

8 
(*proof engine*) 
962bfe78a297
Isar  Intelligible SemiAutomated Reasoning for Isabelle.
wenzelm
parents:
diff
changeset

9 
use "proof_context.ML"; 
962bfe78a297
Isar  Intelligible SemiAutomated Reasoning for Isabelle.
wenzelm
parents:
diff
changeset

10 
use "proof.ML"; 
962bfe78a297
Isar  Intelligible SemiAutomated Reasoning for Isabelle.
wenzelm
parents:
diff
changeset

11 
use "proof_data.ML"; 
6346  12 
use "proof_history.ML"; 
5818
962bfe78a297
Isar  Intelligible SemiAutomated Reasoning for Isabelle.
wenzelm
parents:
diff
changeset

13 
use "args.ML"; 
962bfe78a297
Isar  Intelligible SemiAutomated Reasoning for Isabelle.
wenzelm
parents:
diff
changeset

14 
use "attrib.ML"; 
962bfe78a297
Isar  Intelligible SemiAutomated Reasoning for Isabelle.
wenzelm
parents:
diff
changeset

15 
use "method.ML"; 
6771  16 
use "calculation.ML"; 
5818
962bfe78a297
Isar  Intelligible SemiAutomated Reasoning for Isabelle.
wenzelm
parents:
diff
changeset

17 

962bfe78a297
Isar  Intelligible SemiAutomated Reasoning for Isabelle.
wenzelm
parents:
diff
changeset

18 
(*outer syntax*) 
6549  19 
use "comment.ML"; 
5818
962bfe78a297
Isar  Intelligible SemiAutomated Reasoning for Isabelle.
wenzelm
parents:
diff
changeset

20 
use "outer_lex.ML"; 
962bfe78a297
Isar  Intelligible SemiAutomated Reasoning for Isabelle.
wenzelm
parents:
diff
changeset

21 
use "outer_parse.ML"; 
962bfe78a297
Isar  Intelligible SemiAutomated Reasoning for Isabelle.
wenzelm
parents:
diff
changeset

22 

6346  23 
(*toplevel environment*) 
5818
962bfe78a297
Isar  Intelligible SemiAutomated Reasoning for Isabelle.
wenzelm
parents:
diff
changeset

24 
use "toplevel.ML"; 
6346  25 
use "session.ML"; 
5818
962bfe78a297
Isar  Intelligible SemiAutomated Reasoning for Isabelle.
wenzelm
parents:
diff
changeset

26 

6242  27 
(*theory operations*) 
5818
962bfe78a297
Isar  Intelligible SemiAutomated Reasoning for Isabelle.
wenzelm
parents:
diff
changeset

28 
use "isar_thy.ML"; 
962bfe78a297
Isar  Intelligible SemiAutomated Reasoning for Isabelle.
wenzelm
parents:
diff
changeset

29 
use "isar_cmd.ML"; 
6242  30 

31 
(*theory syntax*) 

32 
use "outer_syntax.ML"; 

5818
962bfe78a297
Isar  Intelligible SemiAutomated Reasoning for Isabelle.
wenzelm
parents:
diff
changeset

33 
use "isar_syn.ML"; 
5873  34 

6242  35 
(*main ML interface*) 
5951  36 
use "isar.ML"; 
5873  37 

38 
structure PureIsar = 

39 
struct 

40 
structure ProofContext = ProofContext; 

41 
structure Proof = Proof; 

6644  42 
structure ProofHistory = ProofHistory; 
5873  43 
structure Args = Args; 
44 
structure Attrib = Attrib; 

45 
structure Method = Method; 

6644  46 
structure Comment = Comment; 
5873  47 
structure OuterLex = OuterLex; 
48 
structure OuterParse = OuterParse; 

49 
structure Toplevel = Toplevel; 

6644  50 
structure Session = Session; 
5873  51 
structure IsarThy = IsarThy; 
52 
structure IsarCmd = IsarCmd; 

6644  53 
structure OuterSyntax = OuterSyntax; 
5873  54 
structure IsarSyn = IsarSyn; 
5951  55 
structure Isar = Isar; 
5873  56 
end; 