abs_def: beta/eta contract lhs;

Added recdef congruence rules for bounded quantifiers and commonly used higher order functions.

various improvements

adjusted to improved code generator interface

added perhaps option combinator

adopted keyword for code generator

Factored out proof for normalization of applications (norm_list).

introduced new map2, fold

typo

simprocs: static evaluation of simpset;

tuned;

tuned msg;

ProofContext.lthms_containing: suppress obvious duplicates;

unfold_tac: static evaluation of simpset;

superceded by timestart|stop.bash;

cpu time = user + system;

replaced lib/scripts/showtime by more advanced lib/scripts/timestart|stop.bash;

assoc_consts and assoc_types now check number of arguments in template.

Added new component "sorts" to record datatype_info.

timestop - report timing based on environment (cf. timestart.bash);

timestart - setup bash environment for timing;

Improved norm_proof to handle proofs containing term (type) variables with same name but different types (sorts): Offending term (type) variables are replaced by dummy (T)Frees before applying the substitution.

restoring the old status of subset_refl

oriented pairs theory * 'a to 'a * theory

initial cleanup to use the new induction method

cleaned up further the proofs (diamond still needs work); changed "fresh:" to "avoiding:"

changed "fresh:" to "avoiding:" and cleaned up the weakening example

match_bind(_i): return terms; mk_def: simultaneous defs; prepare_dummies: produce globally unique indexnames;

method 'fact': SIMPLE_METHOD, i.e. insert facts;

simulaneous 'def';

added facilities to prove the pt and fs instances for discrete types

started to change the transitivity/narrowing case: have trouble with Q=Q.

changed everything until the interesting transitivity_narrowing proof.

minor improvements

modified almost everything for the new nominal_induct (at the end there are some "normal" inductions which need a bit more attention)

Changed order of predicate arguments and quantifiers in strong induction rule.

fixed the lemma where the new names generated by nominal_induct caused problems.

added one clause for substitution in the lambda-case and mad it globally [simp]

added rename_params_rule: recover orginal fresh names in subgoals/cases;

changed induction principle and everything to conform with the new nominal_induct

fresh: frees instead of terms, rename corresponding params in rule; tuned;

adapted to the new nominal_induction

changed \<sim> of permutation equality to \<triangleq> (Jesper wanted to use \<sim>).

fresh_unit_elim and fresh_prod_elim -- for nominal_induct;

reimplement Case expression pattern matching to support lazy patterns

add definitions as defs, not axioms

changed section names

add xsymbol syntax for u type constructor

add constant unit_when

proper treatment of tuple/tuple_fun -- nest to the left!

moved nth_list to Pure/library.ML;

added nth_list;

added mk_split;

changed the order of the induction variable and the context in lam_induct (test to see whether it simplifies the code for nominal_induct).

reworked version with proper support for defs, fixes, fresh specification;

added haskell serializer

exported customized syntax interface

Corrected atom class constraints in strong induction rule.

made some of the theorem look-ups static (by using thm instead of PureThy.get_thm)

added (curried) fold2

added proof of measure_induct_rule;

Added flags for setting and detecting whether a problem needs combinators.

Only output types if !keep_types is true.

Added two functions for CNF translation, used by other files.

Added in four control flags for HOL and FOL translations. Changed functions that perform HOL/FOL translations, and write ATP input to files. Removed some functions that are no longer needed.

Slight modification to trace information.

Added two methods "vampire" and "eprover" that handle both HOL and FOL proofs. Still have old verions of "vampireH","vampireF", "eproverH", "eproverF", which can be called to handle HOL or FOL problems.

Only output arities and class relations if !ResClause.keep_types is true.

some small tuning

ISAR-fied two proofs about equality for abstraction functions.

* Provers/induct: obtain pattern;

added an authors section (please let me know if somebody is left out or unhappy)

some minor tunings

added the version of nominal.thy that contains all properties about support of finite sets

cleaned up all examples so that they work with the current nominal-setting.

finished cleaning up the parts that collect lemmas (with instantiations) under some general names

Corrected treatment of non-recursive abstraction types.

tuned induct proofs;

induct: insert defs in object-logic form; export guess_instance;

tuned induct proofs;

tuned induct proofs;

consume: unfold defs in all major prems;

revert_skolem: fall back on Syntax.deskolem;

forall_conv ~1;

added dummy_pattern;

tuned names;

forall_conv: limit prefix;

fix_tac: proper treatment of major premises in goal; export atomize/rulify interface; tuned;

removed obsolete dummy paragraphs;

tuned;

code generator: case expressions, improved name resolving

added fsub.thy (poplmark challenge) to the examples directory.

Fixed problem with strong induction theorem for datatypes containing no atom types (ind_sort was the empty sort in this case).

send more information with test-takes-too-long message (which tests are still running)

fixed spelling of 'case_conclusion';

tuned induct proofs;