Changed Simplifier.simp_modifiers to Simplifier.simp_modifiers'. This means the syntax of the tactics supports_simp and perm_simp are exactly like simp, namely (supports_simp add: .... del: ...) where the add's and del's are optional.

1) have adjusted the swapping of the result type in add_datatype_i 2) have replaced map_nth_elem by Library.nth_map (there seems to be a clash with an existing nth_map somewhere - therefore the "Library")

tuned;

lthms_containing: not o valid_thms;

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