author  wenzelm 
Tue, 05 Oct 1999 15:34:54 +0200  
changeset 7728  2e737ce3cdb5 
parent 7680  27bbbe36d49a 
child 8091  226dcdc3c5f3 
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"; 
7680  22 
use "obtain.ML"; 
5818
962bfe78a297
Isar  Intelligible SemiAutomated Reasoning for Isabelle.
wenzelm
parents:
diff
changeset

23 

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

24 
(*outer syntax*) 
6549  25 
use "comment.ML"; 
7728  26 
(*use "outer_lex.ML";*) (*see ../Thy/ROOT.ML*) 
5818
962bfe78a297
Isar  Intelligible SemiAutomated Reasoning for Isabelle.
wenzelm
parents:
diff
changeset

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

28 

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

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

32 

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

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

35 
use "isar_cmd.ML"; 
6242  36 

37 
(*theory syntax*) 

38 
use "outer_syntax.ML"; 

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

39 
use "isar_syn.ML"; 
5873  40 

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

44 
structure PureIsar = 

45 
struct 

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

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

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

52 
structure Method = Method; 

7021  53 
structure LocalDefs = LocalDefs; 
54 
structure Calculation = Calculation; 

55 
structure SkipProof = SkipProof; 

7680  56 
structure Obtain = Obtain; 
6644  57 
structure Comment = Comment; 
5873  58 
structure OuterLex = OuterLex; 
59 
structure OuterParse = OuterParse; 

60 
structure Toplevel = Toplevel; 

6644  61 
structure Session = Session; 
5873  62 
structure IsarThy = IsarThy; 
63 
structure IsarCmd = IsarCmd; 

6644  64 
structure OuterSyntax = OuterSyntax; 
5873  65 
structure IsarSyn = IsarSyn; 
5951  66 
structure Isar = Isar; 
5873  67 
end; 