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;

tuned induction proofs;

more robust revert_skolem; tuned;

tuned;

Provers/induct: definitional insts and fixing;

consume: proper treatment of defs; simplified case_conclusion;

added case_conclusion attribute;

(co)induct: taking; induct set: proper treatment of defs;

RuleCases.case_conclusion;

tuned;

added case_conclusion attribute; added coinduct method/attribute; induct method: definsts/fixing/taking; tuned;

improved failure tracking

Datatype_Universe: hide base names only;

added type cases/cases_tactic, and CASES, SUBGOAL_CASES; added consume rule; support named case conclusions; tuned interfaces;

cases_tactic;

moved multi_resolve(s) to drule.ML; cases_tactic;

find_xxxS: term instead of thm;

export map_tags; added multi_resolve(s) -- from Isar/method.ML;

make coinduct actually work; moved some generic code to Pure/Isar/rule_cases.ML; tuned;

Drule.multi_resolves;

declare coinduct rule; tuned;

added code generator syntax

added codegenerator

added code generator syntax

new treatment of polymorphic types, using Sign.const_typargs

added codegen package

added serializer

tweak

fixed some inconveniencies in website

CONJUNCTS;

tuned;

Goal.norm_hhf_protected;

added coinduct attribute; tuned;

added CONJUNCTS: treat conjunction as separate sub-goals;

simpset: added reorient field, set_reorient;

tuned norm_hhf_protected;

removed conj_mono; added conj_curry; tuned;

induct: CONJUNCTS for multiple goals; added coinduct method; tuned;

tuned induct syntax;

FOL: -p 2;