tuned: now using function package

transfer_tac accepts also HOL equations as theorems

shifted min/max to class order

tuned

added class tutorial

code generator changes

generate page labels

definition lookup via terms, not names. Methods "relation" and "lexicographic_order" do not depend on "termination" setup.

declared lemmas true_eqvt and false_eqvt to be equivariant (suggested by samth at ccs.neu.edu)

trying to make single-step proofs work better, especially if they contain abstraction functions. Uniform names for Skolem and Abstraction functions

nominal_inductive no longer proves equivariance.

add a tactic to generate fresh names

simplified ProofContext.infer_types(_pats);

Improved comments.

proper header, added regression tests

added temporary hack to avoid schematic goals in "termination".

Fixes for proof reconstruction, especially involving abstractions and definitions

export is_dummy_pattern;

lemma isCont_inv_fun is same as isCont_inverse_function

moved root and sqrt lemmas from Transcendental.thy to NthRoot.thy

remove use of pos_boundedE

lemma geometric_sum no longer needs class division_by_zero

tuned proofs;

canonical merge operations

added print_indexname; tuned;

improved the equivariance lemmas for the quantifiers; had to export the lemma eqvt_force_add and eqvt_force_del in the thmdecls

added a more usuable lemma for dealing with fresh_fun

generalized type of lemma geometric_sum

replaced read_term_legacy by read_prop_legacy; read: intern_skolem before type-inference (many workarounds!); read: reject_tvars; removed obsolete TypeInfer.logicT -- use dummyT; add_fixes: not constraints for external names;

removed obsolete redeclare_skolems;

read prop as prop, not term;

removed obsolete TypeInfer.logicT -- use dummyT;

avoid internal names;

tuned;

legacy_infer_term/prop -- including intern_term;

Thm.plain_prop_of;

added decode_types (from type_infer.ML); decode sorts: internalize here; tuned;

added read_term; adapted decoding of types/sorts;

added mixfixT (from type_infer.ML);

proper interface infer_types(_pat); Syntax.mixfixT; tuned;

Thm.fold_terms; Syntax.mixfixT;

removed unused Output.panic hook -- internal to PG wrapper;

moved get_sort to sign.ML; moved decode_types to Syntax/type_ext.ML; moved mixfixT to Syntax/mixfix.ML; proper infer_types, without decode/name lookup; tuned;

removed obsolete inferT_axm;

removed obsolete infer_types(_simult); read_sort/get_sort, read_def_terms: internal reorganization;

moved Drule.plain_prop_of, Drule.fold_terms to more_thm.ML;

load type_infer.ML early;

adapted decode_type;

proper ProofContext.infer_types;

Thm.fold_terms;

replaced axioms/finalconsts by proper axiomatization;

simplified read_axm;

tuned comment;

cleaned/simplified Sign.read_typ, Thm.read_cterm etc.; removed dead code;

removed redundant string_of_vname (see term.ML);

removed obsolete read_ctyp, read_def_cterm; moved read_def_cterms, read_cterm to more_thm.ML; avoid rep_theory;

tuned signature; added axiom_table, oracle_table; removed unused read_def_axm;

read_typ_XXX: no sorts; added read_def_typ (formerly read_typ);

added read_def_cterms, read_cterm (from thm.ML);

cleaned/simplified Sign.read_typ, Thm.read_cterm etc.; Term.string_of_vname;