author  wenzelm 
Fri, 09 Jul 1999 18:48:54 +0200  
changeset 6954  dbeafc269f4f 
parent 6888  d0c68ebdabc5 
child 7021  0073aa571502 
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; 

6644  52 
structure Comment = Comment; 
5873  53 
structure OuterLex = OuterLex; 
54 
structure OuterParse = OuterParse; 

55 
structure Toplevel = Toplevel; 

6644  56 
structure Session = Session; 
5873  57 
structure IsarThy = IsarThy; 
58 
structure IsarCmd = IsarCmd; 

6644  59 
structure OuterSyntax = OuterSyntax; 
5873  60 
structure IsarSyn = IsarSyn; 
5951  61 
structure Isar = Isar; 
5873  62 
end; 