doc-src/IsarRef/Thy/document/HOL_Specific.tex
2012-02-10 Cezary Kaliszyk 2012-02-10 more specification of the quotient package in IsarRef
2012-02-10 Cezary Kaliszyk 2012-02-10 specification of the quotient package
2012-02-02 wenzelm 2012-02-02 misc tuning and reformatting; more antiquotations;
2012-02-02 wenzelm 2012-02-02 misc tuning and reformatting;
2011-12-29 wenzelm 2011-12-29 updated generated files;
2011-12-21 bulwahn 2011-12-21 added some basic documentation about method induction_schema extracted from old NEWS
2011-12-21 bulwahn 2011-12-21 adding documentation about the quickcheck_generator command in the IsarRef
2011-12-13 wenzelm 2011-12-13 'datatype' specifications allow explicit sort constraints; tuned signatures;
2011-12-05 kuncar 2011-12-05 merged
2011-12-05 kuncar 2011-12-05 the note about morphisms moved in the description part
2011-12-05 bulwahn 2011-12-05 updating documentation about quiet and verbose options in quickcheck
2011-12-05 bulwahn 2011-12-05 documenting the genuine_only option in quickcheck;
2011-11-30 wenzelm 2011-11-30 discontinued obsolete datatype "alt_names";
2011-11-29 kuncar 2011-11-29 updated documentation for the quotient package
2011-11-08 bulwahn 2011-11-08 adding some documentation about the values command to the isar reference
2011-11-08 bulwahn 2011-11-08 adding a minimal documentation about the code_pred command to the isar reference
2011-10-21 bulwahn 2011-10-21 updating documentation: code_inline -> code_unfold; added documentation about attribute code_unfold_post
2011-10-19 wenzelm 2011-10-19 really document just one code generator;
2011-08-18 bulwahn 2011-08-18 adding documentation about simps equation in the inductive package
2011-08-08 wenzelm 2011-08-08 updated imports;
2011-07-28 noschinl 2011-07-28 document coercions
2011-07-27 bulwahn 2011-07-27 rudimentary documentation of the quotient package in the isar reference manual
2011-07-20 bulwahn 2011-07-20 updating documentation about quickcheck; adding information about try
2011-06-27 blanchet 2011-06-27 document "meson" and "metis" in HOL specific section of the Isar ref manual
2011-06-08 wenzelm 2011-06-08 merged
2011-05-27 blanchet 2011-05-27 document new "try"
2011-06-05 wenzelm 2011-06-05 updated and re-unified classical proof methods; tuned;
2011-06-04 wenzelm 2011-06-04 tuned secref (still dangling);
2011-05-26 wenzelm 2011-05-26 moved/updated basic HOL overview;
2011-05-26 wenzelm 2011-05-26 updated and re-unified (co)inductive definitions in HOL; modernized examples;
2011-05-26 wenzelm 2011-05-26 clarified current 'primrec' vs. old 'recdef'; updated examples from src/HOL/Induct;
2011-05-26 wenzelm 2011-05-26 record examples;
2011-05-26 wenzelm 2011-05-26 updated and simplified HOL datatype examples (NB: special treatment of distinctness has been discontinued in the vicinity of 542b34b178ec);
2011-05-26 wenzelm 2011-05-26 updated and re-unified HOL rep_datatype;
2011-05-25 wenzelm 2011-05-25 rearranged some sections;
2011-05-25 wenzelm 2011-05-25 updated and re-unified HOL typedef, with some live examples;
2011-05-05 wenzelm 2011-05-05 tuned some syntax names;
2011-05-05 wenzelm 2011-05-05 tuned rail diagrams and layout;
2011-05-03 wenzelm 2011-05-03 updated generated files;
2011-05-03 wenzelm 2011-05-03 reactivated codegen example based on Lambda.thy;
2011-05-03 wenzelm 2011-05-03 formal Base theory;
2011-05-02 wenzelm 2011-05-02 simplified rail setup, using plain defaults (NB: \small is incompatible with \isabellestyle used here);
2011-05-02 wenzelm 2011-05-02 moved material about old codegen to isar-ref manual; eliminated old rail diagram;
2011-05-02 wenzelm 2011-05-02 eliminated some duplicate "def" positions;
2011-05-02 wenzelm 2011-05-02 more precise rail diagrams; misc tuning;
2011-05-02 wenzelm 2011-05-02 modernized rail diagrams using @{rail} antiquotation;
2011-04-04 blanchet 2011-04-04 document "nitpick(_params)", "refute(_params)", "try", "sledgehammer(_params)", and "solve_direct"
2011-03-26 wenzelm 2011-03-26 updated generated file; tuned whitespace;
2011-02-25 krauss 2011-02-25 updated generated files
2011-01-11 haftmann 2011-01-11 tuned text
2011-01-11 haftmann 2011-01-11 "enriched_type" replaces less specific "type_lifting"
2010-12-23 haftmann 2010-12-23 documentation stub on type_lifting
2010-12-03 wenzelm 2010-12-03 updated generated file;
2010-11-29 wenzelm 2010-11-29 updated generated files;
2010-11-26 haftmann 2010-11-26 globbing constant expressions use more idiomatic underscore rather than star
2010-11-26 haftmann 2010-11-26 datatype constructor glob for code_reflect
2010-11-08 wenzelm 2010-11-08 updated generated files;
2010-11-06 krauss 2010-11-06 abolished obscure goal variant of [split_format] -- unused (cf. d1c14898fd04), unrelated to '(complete)' variant, and not at all canonical
2010-11-05 wenzelm 2010-11-05 updated generated file, overwriting 55a1693affb6 whose content appears to be in the thy source already;
2010-11-05 bulwahn 2010-11-05 adding documentation of some quickcheck options