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

major refactorings in code generator modules

updated

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

DatatypePackage.case_tac;

DatatypePackage.distinct_simproc;

DatatypePackage.case_tac;

signature cleanup -- no pervasives anymore;

qualified DatatypePackage.distinct_simproc;

adapted case_tac/induct_tac;

updated generated file;

minor typos;

simp: depth_limit is now a configuration option;

removed old AxClass;

remove codegen_process.pdf from distribution;

fixed wrong treatment of type variables in instantiation target

switched to Poly/ML 5.2;

doc test now runs on linux

added at-poly-5.1-para-e;

adjusted location of cambridge website

switch from gtar to tar

send from linux systems as well

tikz: change to pgfsys-dvi.def for plain dvi output;

replaced (*<*)(*>*) by invisibility tags;

updated generated file;

updated generated file;

work within *this* directory;

moved labels into actual sections;

removed TEXPATH, just chdir to Locales/document;

renamed expression: plain ~ (space) instead of \colon;

updated generated file;

replaced strange \: by \colon to make it work again on macbroy20-29;

updated generated file;

clarification of "subst" by Lucas Dixon;

use polyml-5.2;

updated to official 5.2;

use isabelle style files from Doc/ -- not the generated ones (which are not present in the repository anyway);

some reorganization and fine-tuning;

some fine-tuning;

CodeTarget.target_code_width;

Tuned proof.

New version covering interpretation.

proper path to isabelle.jar;

reorganized isar-ref;

added Wenzel:2006:Festschrift;