src/Pure/Isar/ROOT.ML
author haftmann
Thu May 24 08:37:37 2007 +0200 (2007-05-24)
changeset 23086 12320f6e2523
parent 22744 5cbe966d67a2
child 23717 5104b2959ed0
permissions -rw-r--r--
tuned Pure/General/name_space.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 (*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 "../axclass.ML";
    15 use "local_defs.ML";
    16 
    17 (*outer syntax*)
    18 use "outer_lex.ML";
    19 use "args.ML";
    20 use "outer_parse.ML";
    21 use "outer_keyword.ML";
    22 use "antiquote.ML";
    23 
    24 (*theory sources*)
    25 use "../Thy/ml_context.ML";
    26 use "../Thy/thy_load.ML";
    27 use "../Thy/thy_info.ML";
    28 use "../Thy/html.ML";
    29 use "../Thy/latex.ML";
    30 use "../Thy/present.ML";
    31 use "../Thy/thm_deps.ML";
    32 use "../Thy/thm_database.ML";
    33 
    34 (*basic proof engine*)
    35 use "proof_display.ML";
    36 use "attrib.ML";
    37 use "context_rules.ML";
    38 use "skip_proof.ML";
    39 use "method.ML";
    40 use "proof.ML";
    41 use "element.ML";
    42 use "net_rules.ML";
    43 use "induct_attrib.ML";
    44 
    45 (*code generator base*)
    46 use "../Tools/codegen_consts.ML";
    47 use "../Tools/codegen_func.ML";
    48 use "../Tools/codegen_data.ML";
    49 
    50 (*derived theory and proof elements*)
    51 use "local_theory.ML";
    52 use "calculation.ML";
    53 use "obtain.ML";
    54 use "locale.ML";
    55 use "spec_parse.ML";
    56 use "../Tools/class_package.ML";
    57 use "theory_target.ML";
    58 use "specification.ML";
    59 use "constdefs.ML";
    60 
    61 (*toplevel environment*)
    62 use "proof_history.ML";
    63 use "toplevel.ML";
    64 
    65 (*theory presentation*)
    66 use "../Thy/term_style.ML";
    67 use "../Thy/thy_output.ML";
    68 
    69 (*theory syntax*)
    70 use "../Thy/thy_header.ML";
    71 use "session.ML";
    72 use "../old_goals.ML";
    73 use "outer_syntax.ML";
    74 
    75 (*theory and proof operations*)
    76 use "rule_insts.ML";
    77 use "../simplifier.ML";
    78 use "find_theorems.ML";
    79 use "isar_cmd.ML";
    80 use "isar_syn.ML";