proper name for LinearQuantifierElim;

removed old theorem database;

map_const: soft version, no failure here (recovers hiding of consts, because a hidden name is illegal and rejected later);

hide: delete all accesses from extra names -- reduces ambiguity in extern;

map_const: soft version, no failure here;

skolem_fact/thm: uniform numbering, even for singleton list; declare_skofuns: eliminated recovery via Clausify_failure -- should be sufficiently robust as is;

hide (open);

no_notation instead of hide;

* Recovered hiding of consts;

updated generated file;

back to CodeTarget.code_width;

hide -> hide (open)

use regular error function;

add lemma finite_image_approx; remove unnecessary sort annotations

change orientation of fix_eqI and convert to rule_format; add lemma fix_ind2

export just one setup function; more antiquotations; to_nnf: import open, avoiding internal variables (bounds); ThmCache: added table of seen fact names; reorganized skolem_thm/skolem_fact/saturate_skolem_cache: maintain seen fact names, ensure idempotent operation for Theory.at_end; removed obsolete skolem attribute (NB: official fact name unavailable here);

removed obsolete skolem declarations -- done by Theory.at_end;

tuned setup;

remove unnecessary import of Ffun; add lemma admD2

imports Ffun

ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context; eliminated obscure theory merge/transfer -- use explicit theory context instead;

ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;

sane versions of (qualified_)thms_of_thy;

Facts.dest/export_static: content difference; tuned;

dest/export_static: content difference; tuned comments;

declare_skofuns/skolem: canonical argument order; minor tuning;

Facts.dest/export_static: content difference;

correction

tuned

Removed hide swap

fixed type

lemma modified

typo

had to add rule: because induct_tac no longer works correctly

Hid swap

some reformatting;

added CK_Machine to the nominal section

soundness and completeness proofs for a CK machine as well as proofs for type preservation

emoved the parts that deal with the CK machine to a new theory

tuned header and comments

OldGoals.inst;

Drule.read_instantiate; Drule.types_sorts;

qualified inst;

qualified types_sorts, read_insts etc.;

Drule.types_sorts;

OldGoals.inst;

Drule.read_instantiate;

changed pred_congs: merely cover pred1_cong pred2_cong pred3_cong;

removed obsolete/unused pred_congs;

tuned comments;

converted ML proofs from simpdata.ML; tuned;

removed dead code;

RuleInsts.res_inst_tac with proper context;

more antiquotations;

tuned;

explicit rule for induct_tac

tuned spacing;

updated generated file;

* Attributes cases, induct, coinduct support del option.

added del attributes; tuned;

back to original import order -- thanks to proper deletion of nat cases/induct rules from type_definition;

proper deletion of nat cases/induct rules from type_definition;

fixed spelling (Where is WordExamples.thy anyway?);

recovered nat_induct as default for induct_tac;

more robust declaration of nat_induct;

reordering of imports ensures that nat_induct stay in front;

adhoc fix of induct_tac: rule nat_induct;

case_tac: accomodate change in bound variable name;

nat_induct_tac (works without context);

moved case_tac/induct_tac to induct_tacs.ML -- no longer hardwired into datatype package;

added nat_induct_tac (works without context);

InductTacs.case_tac with proper context and proper declaration of local variable;

added HOL/Tools/induct_tacs.ML;

eliminated obsolete case_split_thm -- use case_split; added case_split_tac (works without context); setup for induct_tacs.ML;

tuned proofs -- case_tac *is* available here;

updated generated file;

case_tac/induct_tac: use same declarations as cases/induct;

proper news header; methods case_tac and induct_tac now refer to usual declarations; removed obsolete induct_tac and thm_induct_tac;

removed obsolete read_idents;

added (e)res_inst_tac; tuned comments;

focus: actually declare constraints for local parameters;

tuned proofs;

case_split_tac (works without context);

tuned;

eliminated obsolete case_split_thm -- use case_split;

Unstructured induction and cases analysis for Isabelle/HOL.

dropped instance with attached definitions

polished interface of datatype package

adjusted some proofs involving inats

refactoring; addition, numerals

more instantiation

whitespace tuning

localized Least in Orderings.thy

removed some dubious code lemmas

slightly tuning of some proofs involving case distinction and induction on natural numbers and similar

rep_datatype command now takes list of constructors as input arguments