author  wenzelm 
Tue, 24 Nov 1998 11:59:50 +0100  
changeset 5951  e98c900540f9 
parent 5873  f4fe91b3b6db 
child 6242  3d75f5a99f60 
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"; 
962bfe78a297
Isar  Intelligible SemiAutomated Reasoning for Isabelle.
wenzelm
parents:
diff
changeset

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

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

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

15 

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

16 
(*outer syntax*) 
962bfe78a297
Isar  Intelligible SemiAutomated Reasoning for Isabelle.
wenzelm
parents:
diff
changeset

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

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

19 

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

20 
(*interactive subsystem*) 
962bfe78a297
Isar  Intelligible SemiAutomated Reasoning for Isabelle.
wenzelm
parents:
diff
changeset

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

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

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

24 

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

25 
(*theory operations and syntax*) 
962bfe78a297
Isar  Intelligible SemiAutomated Reasoning for Isabelle.
wenzelm
parents:
diff
changeset

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

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

28 
use "isar_syn.ML"; 
5873  29 

5951  30 
(*main interface*) 
31 
use "isar.ML"; 

5873  32 

33 
structure PureIsar = 

34 
struct 

35 
structure ProofContext = ProofContext; 

36 
structure Proof = Proof; 

37 
structure Args = Args; 

38 
structure Attrib = Attrib; 

39 
structure Method = Method; 

40 
structure OuterLex = OuterLex; 

41 
structure OuterParse = OuterParse; 

42 
structure ProofHistory = ProofHistory; 

43 
structure Toplevel = Toplevel; 

44 
structure OuterSyntax = OuterSyntax; 

45 
structure IsarThy = IsarThy; 

46 
structure IsarCmd = IsarCmd; 

47 
structure IsarSyn = IsarSyn; 

5951  48 
structure Isar = Isar; 
5873  49 
end; 