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.