src/Pure/Isar/ROOT.ML
author haftmann
Fri Nov 10 07:44:47 2006 +0100 (2006-11-10)
changeset 21286 b5e7b80caa6a
parent 20880 b853d4326894
child 21350 6e58289b6685
permissions -rw-r--r--
introduces canonical AList functions for loop_tacs
     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 (*proof context*)
     9 use "object_logic.ML";
    10 use "rule_cases.ML";
    11 use "auto_bind.ML";
    12 use "local_syntax.ML";
    13 use "proof_context.ML";
    14 use "local_defs.ML";
    15 
    16 (*theory presentation*)
    17 use "../Thy/html.ML";
    18 use "../Thy/latex.ML";
    19 use "../Thy/present.ML";
    20 use "../Thy/thm_deps.ML";
    21 use "../Thy/thm_database.ML";
    22 
    23 (*basic proof engine*)
    24 use "proof_display.ML";
    25 use "args.ML";
    26 use "attrib.ML";
    27 use "context_rules.ML";
    28 use "skip_proof.ML";
    29 use "method.ML";
    30 use "proof.ML";
    31 use "element.ML";
    32 use "net_rules.ML";
    33 use "induct_attrib.ML";
    34 
    35 (*derived theory and proof elements*)
    36 use "local_theory.ML";
    37 use "calculation.ML";
    38 use "obtain.ML";
    39 use "locale.ML";
    40 use "../axclass.ML";
    41 use "theory_target.ML";
    42 use "specification.ML";
    43 use "constdefs.ML";
    44 
    45 (*outer syntax*)
    46 use "antiquote.ML";
    47 use "outer_parse.ML";
    48 use "outer_keyword.ML";
    49 
    50 (*toplevel environment*)
    51 use "proof_history.ML";
    52 use "toplevel.ML";
    53 
    54 (*theory presentation*)
    55 use "term_style.ML";
    56 use "isar_output.ML";
    57 
    58 (*theory syntax*)
    59 use "thy_header.ML";
    60 use "session.ML";
    61 use "../old_goals.ML";
    62 use "outer_syntax.ML";
    63 
    64 (*theory and proof operations*)
    65 use "rule_insts.ML";
    66 use "../simplifier.ML";
    67 use "find_theorems.ML";
    68 use "isar_thy.ML";
    69 use "isar_cmd.ML";
    70 use "isar_syn.ML";