tuned

added an Isar-proof for the abs_ALL lemma

tuning

defines: beta/eta contract lhs; replaced type_syntax by mixfix_type, which handles binders as well;

asts_to_terms: builtin free_fixed translation makes local binders work properly;

mixfix_args: 1 for binders; string_of_mixfix: proper output of binders;

removed fixed_tr: now handled in syntax module; replaced mixfix_typ by TypeInfer.mixfixT, which handles binders as well; def: beta/eta contract lhs;

added mixfixT; paramify_dummies: treat dummyT as well, tuned;

defs: beta/eta contract lhs;

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