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;

cleaned/simplified Sign.read_typ, Thm.read_cterm etc.; avoid rep_theory;

removed Pure/Syntax/ROOT.ML;

Term.string_of_vname;

Theory.inferT_axm;

do not enable Toplevel.debug globally;

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

canonical merge operations

declarations: apply target_morphism;

inst(T)_morphism: avoid reference to static theory value;

tuned signature; export: precomputed closure, no reference to contexts;

added Morphism.transform/form (generic non-sense);

Morphism.transform/form;

data declaration: removed obsolete target_morphism (still required for local data!?);

data declaration: removed obsolete target_morphism;

added eval_antiquotes_fn (tmp);

tuned document (headers, sections, spacing);

do translation: CONST;

eval_antiquotes: proper parentheses for projection;

canonical merge operations

Removed erroneous application of rev in get_clauses that caused introduction rules taken from the InductivePackage database to be in the wrong order.

more robust proof

Experimental code for the interpretation of definitions.

Experimental interpretation code for definitions.