author  wenzelm 
Fri, 16 Jul 1999 22:22:02 +0200  
changeset 7021  0073aa571502 
parent 6954  dbeafc269f4f 
child 7680  27bbbe36d49a 
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 

6888
d0c68ebdabc5
skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
6783
diff
changeset

8 
(*basic proof engine*) 
6783
9cf9c17d9e35
renamed object_logic.ML to Isar/auto_bind.ML and tuned this module;
wenzelm
parents:
6771
diff
changeset

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

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

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

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

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

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

16 
use "method.ML"; 
6888
d0c68ebdabc5
skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
6783
diff
changeset

17 

d0c68ebdabc5
skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
6783
diff
changeset

18 
(*derived proof elements*) 
6954  19 
use "local_defs.ML"; 
6771  20 
use "calculation.ML"; 
6888
d0c68ebdabc5
skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
6783
diff
changeset

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

22 

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

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

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

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

27 

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

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

31 

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

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

34 
use "isar_cmd.ML"; 
6242  35 

36 
(*theory syntax*) 

37 
use "outer_syntax.ML"; 

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

38 
use "isar_syn.ML"; 
5873  39 

6242  40 
(*main ML interface*) 
5951  41 
use "isar.ML"; 
5873  42 

43 
structure PureIsar = 

44 
struct 

6783
9cf9c17d9e35
renamed object_logic.ML to Isar/auto_bind.ML and tuned this module;
wenzelm
parents:
6771
diff
changeset

45 
structure AutoBind = AutoBind; 
5873  46 
structure ProofContext = ProofContext; 
47 
structure Proof = Proof; 

6644  48 
structure ProofHistory = ProofHistory; 
5873  49 
structure Args = Args; 
50 
structure Attrib = Attrib; 

51 
structure Method = Method; 

7021  52 
structure LocalDefs = LocalDefs; 
53 
structure Calculation = Calculation; 

54 
structure SkipProof = SkipProof; 

6644  55 
structure Comment = Comment; 
5873  56 
structure OuterLex = OuterLex; 
57 
structure OuterParse = OuterParse; 

58 
structure Toplevel = Toplevel; 

6644  59 
structure Session = Session; 
5873  60 
structure IsarThy = IsarThy; 
61 
structure IsarCmd = IsarCmd; 

6644  62 
structure OuterSyntax = OuterSyntax; 
5873  63 
structure IsarSyn = IsarSyn; 
5951  64 
structure Isar = Isar; 
5873  65 
end; 