(* Title: Pure/Isar/ROOT.ML ID: $Id$ Author: Markus Wenzel, TU Muenchen Isar -- Intelligible Semi-Automated Reasoning for Isabelle. *) (*proof context*) use "object_logic.ML"; use "rule_cases.ML"; use "auto_bind.ML"; use "local_syntax.ML"; use "proof_context.ML"; use "../axclass.ML"; use "local_defs.ML"; (*outer syntax*) use "outer_lex.ML"; use "args.ML"; use "outer_parse.ML"; use "outer_keyword.ML"; use "antiquote.ML"; (*theory sources*) use "../Thy/ml_context.ML"; use "../Thy/thy_load.ML"; use "../Thy/thy_info.ML"; use "../Thy/html.ML"; use "../Thy/latex.ML"; use "../Thy/present.ML"; use "../Thy/thm_deps.ML"; use "../Thy/thm_database.ML"; (*basic proof engine*) use "proof_display.ML"; use "attrib.ML"; use "context_rules.ML"; use "skip_proof.ML"; use "method.ML"; use "proof.ML"; use "element.ML"; use "net_rules.ML"; use "induct_attrib.ML"; (*code generator base*) use "../Tools/codegen_consts.ML"; use "../Tools/codegen_func.ML"; use "../Tools/codegen_data.ML"; (*derived theory and proof elements*) use "local_theory.ML"; use "calculation.ML"; use "obtain.ML"; use "locale.ML"; use "spec_parse.ML"; use "../Tools/class_package.ML"; use "theory_target.ML"; use "specification.ML"; use "constdefs.ML"; (*toplevel environment*) use "proof_history.ML"; use "toplevel.ML"; (*theory presentation*) use "../Thy/term_style.ML"; use "../Thy/thy_output.ML"; (*theory syntax*) use "../Thy/thy_header.ML"; use "session.ML"; use "../old_goals.ML"; use "outer_syntax.ML"; (*theory and proof operations*) use "rule_insts.ML"; use "../simplifier.ML"; use "find_theorems.ML"; use "isar_cmd.ML"; use "isar_syn.ML";