# HG changeset patch # User berghofe # Date 999266781 -7200 # Node ID ec89f5cff390573414d5adee4ecd5db6dc39f258 # Parent c6dd19025abeda7e03781ed5a3cc4974fe4829d3 Added new files for proof terms. diff -r c6dd19025abe -r ec89f5cff390 src/Pure/IsaMakefile --- a/src/Pure/IsaMakefile Thu Aug 30 22:51:11 2001 +0200 +++ b/src/Pure/IsaMakefile Fri Aug 31 16:06:21 2001 +0200 @@ -38,14 +38,17 @@ Isar/session.ML Isar/skip_proof.ML Isar/thy_header.ML Isar/toplevel.ML \ ML-Systems/mlworks.ML ML-Systems/polyml.ML ML-Systems/polyml-3.x.ML ML-Systems/smlnj-0.93.ML \ ML-Systems/smlnj.ML ROOT.ML Syntax/ROOT.ML Syntax/ast.ML \ + Proof/ROOT.ML Proof/proofchecker.ML Proof/proof_rewrite_rules.ML \ + Proof/proof_syntax.ML Proof/reconstruct.ML \ Syntax/lexicon.ML Syntax/mixfix.ML Syntax/parser.ML \ Syntax/printer.ML Syntax/syn_ext.ML Syntax/syn_trans.ML \ Syntax/syntax.ML Syntax/token_trans.ML Syntax/type_ext.ML \ Thy/ROOT.ML Thy/html.ML Thy/latex.ML Thy/present.ML Thy/thm_deps.ML \ Thy/thm_database.ML Thy/thy_info.ML Thy/thy_load.ML Thy/thy_parse.ML \ Thy/thy_scan.ML Thy/thy_syn.ML axclass.ML basis.ML context.ML \ - deriv.ML display.ML drule.ML envir.ML goals.ML install_pp.ML \ - library.ML locale.ML logic.ML meta_simplifier.ML net.ML pattern.ML pure.ML pure_thy.ML \ + codegen.ML display.ML drule.ML envir.ML goals.ML install_pp.ML \ + library.ML locale.ML logic.ML meta_simplifier.ML net.ML pattern.ML \ + proofterm.ML pure.ML pure_thy.ML \ search.ML sign.ML sorts.ML tactic.ML tctical.ML term.ML theory.ML \ theory_data.ML thm.ML type.ML type_infer.ML unify.ML @./mk diff -r c6dd19025abe -r ec89f5cff390 src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Thu Aug 30 22:51:11 2001 +0200 +++ b/src/Pure/ROOT.ML Fri Aug 31 16:06:21 2001 +0200 @@ -7,7 +7,7 @@ *) val banner = "Pure Isabelle"; -val version = "Isabelle repository version"; (*filled in automatically!*) +val version = "Isabelle repository"; print_depth 1; @@ -38,10 +38,10 @@ use "theory.ML"; use "theory_data.ML"; use "context.ML"; +use "proofterm.ML"; use "thm.ML"; use "display.ML"; use "pure_thy.ML"; -use "deriv.ML"; use "drule.ML"; use "meta_simplifier.ML"; use "locale.ML"; @@ -50,6 +50,14 @@ use "tactic.ML"; use "goals.ML"; +(*proof term operations*) +cd "Proof"; +use "reconstruct.ML"; +use "proof_syntax.ML"; +use "proof_rewrite_rules.ML"; +use "proofchecker.ML"; +cd ".."; + (*theory system operations*) cd "Thy"; use "ROOT.ML"; cd ".."; @@ -58,6 +66,9 @@ use "axclass.ML"; +(*code generator*) +use "codegen.ML"; + (*external interfaces*) cd "Interface"; use "ROOT.ML"; cd ".."; @@ -82,3 +93,4 @@ print_depth 8; ml_prompts "ML> " "ML# "; +