src/Pure/Isar/ROOT.ML
author wenzelm
Sat Jan 07 23:27:52 2006 +0100 (2006-01-07)
changeset 18613 3cdfa57408be
parent 18604 4000f368dc7f
child 18634 1dc034c3df61
permissions -rw-r--r--
added Isar/specification.ML;
     1 (*  Title:      Pure/Isar/ROOT.ML
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4 
     5 Isar -- Intelligible Semi-Automated Reasoning for Isabelle.
     6 *)
     7 
     8 (*basic proof engine*)
     9 use "object_logic.ML";
    10 use "rule_cases.ML";
    11 use "auto_bind.ML";
    12 use "proof_context.ML";
    13 use "proof_display.ML";
    14 use "context_rules.ML";
    15 use "args.ML";
    16 use "attrib.ML";
    17 use "skip_proof.ML";
    18 use "method.ML";
    19 use "proof.ML";
    20 use "element.ML";
    21 use "net_rules.ML";
    22 use "induct_attrib.ML";
    23 
    24 (*derived theory and proof elements*)
    25 use "specification.ML";
    26 use "constdefs.ML";
    27 use "obtain.ML";
    28 use "locale.ML";
    29 use "calculation.ML";
    30 
    31 (*outer syntax*)
    32 use "antiquote.ML";
    33 use "outer_parse.ML";
    34 use "outer_keyword.ML";
    35 
    36 (*toplevel environment*)
    37 use "proof_history.ML";
    38 use "toplevel.ML";
    39 
    40 (*theory presentation*)
    41 use "term_style.ML";
    42 use "isar_output.ML";
    43 
    44 (*theory syntax*)
    45 use "thy_header.ML";
    46 use "session.ML";
    47 use "../old_goals.ML";
    48 use "outer_syntax.ML";
    49 
    50 (*theory and proof operations*)
    51 use "../simplifier.ML";
    52 use "find_theorems.ML";
    53 use "isar_thy.ML";
    54 use "isar_cmd.ML";
    55 use "isar_syn.ML";