author  wenzelm 
Fri, 30 Apr 1999 18:04:42 +0200  
changeset 6549  90fa592f6e6e 
parent 6346  643a1bd31a91 
child 6644  123b215882ae 
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"; 
962bfe78a297
Isar  Intelligible SemiAutomated Reasoning for Isabelle.
wenzelm
parents:
diff
changeset

16 

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

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

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

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

21 

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

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

25 

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

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

28 
use "isar_cmd.ML"; 
6242  29 

30 
(*theory syntax*) 

31 
use "outer_syntax.ML"; 

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

32 
use "isar_syn.ML"; 
5873  33 

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

37 
structure PureIsar = 

38 
struct 

39 
structure ProofContext = ProofContext; 

40 
structure Proof = Proof; 

41 
structure Args = Args; 

42 
structure Attrib = Attrib; 

43 
structure Method = Method; 

44 
structure OuterLex = OuterLex; 

45 
structure OuterParse = OuterParse; 

46 
structure ProofHistory = ProofHistory; 

47 
structure Toplevel = Toplevel; 

48 
structure OuterSyntax = OuterSyntax; 

49 
structure IsarThy = IsarThy; 

50 
structure IsarCmd = IsarCmd; 

51 
structure IsarSyn = IsarSyn; 

5951  52 
structure Isar = Isar; 
5873  53 
end; 