added fact_tac, some_fact_tac; retrieve_thms: support literal facts; tuned export interfaces;

renamed Goal constant to prop, more general protect/unprotect interfaces; tuned ProofContext.export interfaces;

renamed Goal constant to prop, more general protect/unprotect interfaces;

added fact method; accomodate simplified Thm.lift_rule;

tuned ProofContext.export interfaces;

syntax for literal facts;

removed try_dest_Goal, use Logic.unprotect;

added cgoal_of; simplified lift_rule: take goal cterm instead of goal state thm, use Logic.lift_abs/all;

accomodate simplified Thm.lift_rule; tuned;

export cong_modifiers, simp_modifiers';

certify_term: tuned monomorphic consts;

datatype thmref: added Fact; renamed Goal constant to prop;

Logic.lift_all;

renamed Goal constant to prop, more general protect/unprotect interfaces; replaced lift_fns by lift_abs, lift_all;

renamed Goal.norm_hhf_rule to Goal.norm_hhf;

renamed Goal constant to prop, more general protect/unprotect interfaces; renamed norm_hhf_rule to norm_hhf; added comp_hhf, compose_hhf_tac, based on Drule.lift_all;

added add_local/add_global; index props (for add_local only); added could_unify;

added incr_indexes; added lift_all (approx. reverse of gen_all); renamed Goal constant to prop, more general protect/unprotect interfaces;

renamed Goal constant to prop;

accomodate simplified Thm.lift_rule;

Logic.unprotect;

literal facts;

* Pure/Isar: literal facts; * ML/Pure: tuned Thm.lift_rule; * ML/Pure: renamed Goal constant to prop, more general uses;

tuned;

unnecessary imports removed

fixed case names in the weak induction principle and changed name from "induct" to "induct_weak"

Implemented proof of weak induction theorem.

Added "deepen" method.

circumvented smlnj value restriction

added extraction interface for code generator

Added (optional) arguments to the tactics perm_eq_simp and supports_simp. They now follow the "simp"-way and use the syntax: apply(supports_simp simp add: thms) etc.

cleaned up nth, nth_update, nth_map and nth_string functions

Removed legacy prove_goalw_cterm command.

got rid of obsolete prove_goalw_cterm

swapped add_datatype result

removed obfuscating PStrStrTab

reachable - abandoned foldl_map in favor of fold_map

Added Tools/res_hol_clause.ML

Added a new file res_hol_clause.ML to Reconstruction.thy. This file is used to translate HOL formulae into FOL clauses.

Added "writeln_strs" to the signature

Added several new functions that are used to prove HOL goals. Added new methods "vampireH" and "eproverH" that can prove both FOL and HOL goals. The old "vampire" and "eprover" methods are renamed to "vampireF" and "eproverF"; they can only prove FOL goals.

Added new functions to handle HOL goals and lemmas. Added a funtion to send types and sorts information to ATP: they are clauses written to a separate file. Removed several functions definitions, and combined them with those in other files.

Added several new functions that convert HOL Isabelle rules to FOL axiom clauses. The original functions that convert FOL rules to clauses stay with the same names; the new functions have "H" at the end of their names. Also added function "repeat_RS" to the signature.

Added several functions to the signature. Added two new functions, which are used by res_hol_clause.ML programs.

A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.

sorted lemma lists

* HOL: alternative iff syntax;

consts: monomorphic;

removed inappropriate monomorphic test;

replaced Defs.monomorphic by Sign.monomorphic;

alternative iff syntax for equality on booleans, with print_mode 'iff';

added module Pure/General/rat.ML

tidied away duplicate thm

EVERY;

traceIt: plain term;

val legacy = ref false;

prove_raw: cterms, explicit asms; prove: Pattern.matches beta_norm;

avoid legacy goals;

legacy = ref true for the time being -- avoid volumious warnings;

tuned;

avoid OldGoals shortcuts;

* Legacy goal package: reduced interface to the bare minimum required to keep existing proof scripts running. * Internal goals: structure Goal.

Internal goals.

renamed triv_goal to goalI, rev_triv_goal to goalD;

tuned header;

Goal.norm_hhf_rule;

export add_binds_i; invoke_case: AutoBind.no_facts; Goal.init, Goal.conclude;

load_file: setmp OldGoals.legacy true;

improved check_result; Goal.init, Goal.conclude;

Goal.prove_plain;

do not export find_thms;

use obsolete goals.ML here;

Goal.conclude;

moved SELECT_GOAL to goal.ML;

moved norm_hhf_rule, prove etc. to goal.ML; moved asm_rewrite_goal_tac to simplifier.ML;

added simplification tactics and rules (from meta_simplifier.ML);

moved various simplification tactics and rules to simplifier.ML;

warn_obsolete for goal commands -- danger of disrupting a local proof context; Goal.init, Goal.conclude, Goal.norm_hhf_rule; shortcuts no longer pervasive (cf. structure OldGoals);

renamed triv_goal to goalI, rev_triv_goal to goalD; removed mk_triv_goal (cf. Goal.init);

added goal.ML; moved use of goals.ML;

added goal.ML;

Goal.norm_hhf_rule, Goal.init;

avoid triv_goal and home-grown meta_allE;

OldGoals;

proper header; proper use of ML files;

avoid home-grown meta_allE;

Goal.prove;

avoid shortcuts from OldGoals;

added simplified settings for Poly/ML 4.x (commented out);

reverted (accidental?) change of 1.148;

abandoned rational number functions in favor of General/rat.ML

introduced functions from Pure/General/rat.ML

slight corrections

substantially improved integration of website into distribution framework

substantially improved integration of website into distribution framework

substantially improved integration of website into distribution framework

substantially improved integration of website into distribution framework

towards an improved website/makedist integration

towards an improved website/makedist integration

added default distinfo.mak

towards an improved website/makedist integration

towards an improved website/makedist integration

added rounding functions

Merged theory ResAtpOracle.thy into ResAtpMethods.thy

obsolete;

removed add_inductive_x;

removed obsolete add_datatype_x; tuned;

removed obsolete thy_syntax.ML;

removed obsolete old_symbol_source;

removed obsolete non-Isar theory format and old Isar theory headers;

removed old-style theory format; tuned;

avoid lagacy read function;

added thm(s) retrieval functions (from goals.ML);

removed obsolete old-locales; moved thm(s) retrieval functions back to pure_thy.ML; removed atomic_goal(w) interface; removed user-level (top_sg, prin, printyp, pprint_term/typ, which tend to cause some confusion about the implicit goal (!) context being used here;

removed obsolete axclass_tac, add_inst_subclass_x, add_inst_arity_x;

removed obsolete Thy/thy_parse.ML, Thy/thy_scan.ML, Thy/thy_syn.ML;

removed obsolete old-style syntax;

removed obsolete IOA/meta_theory/ioa_package.ML;

removed obsolete domain/interface.ML, IOA/meta_theory/ioa_package.ML;

removed obsolete domain/interface.ML;