HOL/Tools/function_package: More cleanup

export read/cert_expr; moved type witness to element.ML (abstract type); tuned;

guess: more careful about local polymorphism; guess: explicit term vars in statement (avoids warning);

assm_tac: try rule termI;

added params_of, prems_of; added type witness (from locale.ML); misc cleanup;

added matches_seq (left-to-right matching, intermediate beta-normalization);

support embedded terms;

allow non-trivial schematic goals (via embedded term vars);

HOL/Tools/fundef_package: Cleanup

added some further lemmas that deal with permutations and set-operators

added the lemma perm_diff

HOL/Tools/function_package: Added support for mutual recursive definitions.

Added [simp]-lemmas "in_inv_image" and "in_lex_prod" in the spirit of "in_measure". This simplifies some proofs.

ATP/res_clasimpset.ML has been merged into res_atp.ML.

Functions of Tools/ATP/res_clasimpset.ML are now in Tools/res_atp.ML. res_clasimpset.ML is not used anymore.

generalized wfI

misc cleanup;

removed obsolete ML files;

tuned;

tuned;

removed obsolete ML files;

merge: always normalize (and check!) reductions;

removed legacy ML scripts

tuned;

removed obsolete ML files;

lemmas strip;

removed obsolete ML files;

added some installation notes for the nominal package

Tiny code cleanup

added an example suggested by D. Wang on the PoplMark-mailing list; it shows how the height of an alpha-equated lambda term interacts with capture-avoiding substitution

added the hack "reset NameSpace.unique_names" to Nominal.thy (Stefan is working on a real fix in the nominal_package)

tuned type print-translations ----------------------------------------------------------------------

proper meta definition;

fixed bug in type print translations

tuned;

warnings to debug outputs

warnings to debug outputs; default translation to const-typed

Giving the "--silent" switch to E, to produce less output

fixing a variable-clash bug in rule_by_tactic

removed legacy ML scripts;

removed legacy ML scripts;

removed legacy ML scripts;

removed legacy ML scripts;

removed legacy ML scripts;

tuned;

tuned;

complete_split_rule: all Vars; tuned;

unfold/refold: LocalDefs.meta_rewrite_rule; ObjectLogic.full_atomize_tac; tuned;

removed unused extern_thm;

activate Defines: fix frees;

pretty: do not exterm thm names;

forall_intr_list: do not ignore errors;

separate checks for acyclic/wellformed;

freeze_spec: gensym;

tuned;

axiomatization java_lang;

Changed the DFG format's functions' declaration procedure.

Fixed a bug.

A new "spass" method.

Added in settings used by "spass" method.

Added in SPASS oracle.

HOL problems now have DFG output format.

Changed input interface of dfg_write_file.

Added support for DFG format, used by SPASS.

Helper files in DFG format.

add_datatype_axm: finalize specified consts;

tuned;

tuned;

made smlnj happy;

wellformed: be less ambitious about structural containment; tuned;

Pure: update on overloaded defs;

Extended strong induction rule with additional freshness constraints.

add theorem cfcomp_strict

added add_deps, which actually records dependencies of consts (unlike add_finals); tuned;

tuned;

axiomatize class: Theory.add_deps;

simplified info/get_info; Rep/Abs: Theory.add_deps; tuned;

simplified TypedefPackage.get_info;

made smlnj happy;

pretty_full_theory: tuned output of definitions;

export plain_args; tuned wellformed, normalize;

Defs.specifications_of: lhs/rhs now use typargs;

removed unchecked'';

pretty_full_theory: defs;

specifications_of: lhs/rhs represented as typargs; export pretty_const; export dest; more precise checking of lhs patterns; more precise normalization; misc cleanup;

export raw_unifys, could_unifys;

made smlnj happy;

export raw_matches;

tuned Defs interfaces;

yet another re-implementation: . maintain explicit mapping from unspecified to specified consts (no dependency graph, no termination check, but direct reduction of specifications); . more precise checking of LHS patterns -- specialized patterns (e.g. 'a => 'a instead of general 'a => 'b) impose global restrictions;

removed obsolete partition (cf. List.partition); tuned;

class axiomatization: finals;

abs: precise typing;

added syntax for 'unchecked';

primrec (unchecked);

List.partition;

ax_derivs: precise typing;

pow: unchecked;

removed obsolete 'finalconsts';

* Pure: syntax 'CONST name' produces a fully internalized constant; tuned;

added CONST syntax; tuned interfaces;

export generic term_syntax;

consts: replaced early'' flag by inverted authentic''; tuned interfaces;

added mapping;

replaced early'' flag by inverted authentic'';

renamed CONST to CONSTANT;

removing the string array from the result of get_clasimp_atp_lemmas

const_syntax;

always preserve authentic consts -- removed Syntax.mixfix_const;

tuned;

removed outdated/redundant comments;

prefer 'definition' over low-level defs; tuned source/document;

tuned source/document;

hide const subst;

tuned;

const_syntax;

* Isar/locale: 'const_syntax';

added const_syntax(_i);

export consts_of; added add_const_syntax; tuned interface;

replaced abbrevs by term_syntax, which is both simpler and more general;