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;
wenzelm@5818
     1
(*  Title:      Pure/Isar/ROOT.ML
wenzelm@5818
     2
    ID:         $Id$
wenzelm@5818
     3
    Author:     Markus Wenzel, TU Muenchen
wenzelm@5818
     4
wenzelm@5818
     5
Isar -- Intelligible Semi-Automated Reasoning for Isabelle.
wenzelm@5818
     6
*)
wenzelm@5818
     7
wenzelm@6888
     8
(*basic proof engine*)
wenzelm@11889
     9
use "object_logic.ML";
wenzelm@17348
    10
use "rule_cases.ML";
wenzelm@6783
    11
use "auto_bind.ML";
wenzelm@5818
    12
use "proof_context.ML";
wenzelm@17348
    13
use "proof_display.ML";
wenzelm@13369
    14
use "context_rules.ML";
wenzelm@15703
    15
use "args.ML";
wenzelm@15703
    16
use "attrib.ML";
wenzelm@17348
    17
use "skip_proof.ML";
wenzelm@17103
    18
use "method.ML";
wenzelm@5818
    19
use "proof.ML";
wenzelm@18128
    20
use "element.ML";
wenzelm@8298
    21
use "net_rules.ML";
wenzelm@11658
    22
use "induct_attrib.ML";
wenzelm@6888
    23
wenzelm@17348
    24
(*derived theory and proof elements*)
wenzelm@18613
    25
use "specification.ML";
wenzelm@17348
    26
use "constdefs.ML";
wenzelm@18604
    27
use "obtain.ML";
wenzelm@17348
    28
use "locale.ML";
wenzelm@6771
    29
use "calculation.ML";
wenzelm@5818
    30
wenzelm@5818
    31
(*outer syntax*)
wenzelm@9125
    32
use "antiquote.ML";
wenzelm@5818
    33
use "outer_parse.ML";
wenzelm@17058
    34
use "outer_keyword.ML";
wenzelm@5818
    35
wenzelm@6346
    36
(*toplevel environment*)
wenzelm@17348
    37
use "proof_history.ML";
wenzelm@5818
    38
use "toplevel.ML";
wenzelm@17058
    39
wenzelm@17058
    40
(*theory presentation*)
haftmann@15918
    41
use "term_style.ML";
berghofe@15434
    42
use "isar_output.ML";
wenzelm@5818
    43
wenzelm@12936
    44
(*theory syntax*)
wenzelm@12936
    45
use "thy_header.ML";
wenzelm@17058
    46
use "session.ML";
wenzelm@18116
    47
use "../old_goals.ML";
wenzelm@12936
    48
use "outer_syntax.ML";
wenzelm@12936
    49
wenzelm@8091
    50
(*theory and proof operations*)
wenzelm@16025
    51
use "../simplifier.ML";
wenzelm@16025
    52
use "find_theorems.ML";
wenzelm@17348
    53
use "isar_thy.ML";
wenzelm@5818
    54
use "isar_cmd.ML";
wenzelm@5818
    55
use "isar_syn.ML";