doc-src/IsarRef/Thy/HOL_Specific.thy
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 haftmann 2011-12-29 attribute code_abbrev superseedes code_unfold_post
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-10-19 bulwahn 2011-10-19 removing documentation about the old 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-05-27 blanchet 2011-05-27 removed FIXME: "try_methods" doesn't take a clasimpmod, because it needs to generate Isar proof text in case of success and hence needs total control over its arguments
2011-05-27 blanchet 2011-05-27 renamed "try" "try_methods"
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 reactivated codegen example based on Lambda.thy;
2011-05-03 wenzelm 2011-05-03 formal Base theory;
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-03-23 bulwahn 2011-03-23 adding documentation about the eval option in quickcheck
2011-02-25 krauss 2011-02-25 removed support for tail-recursion from function package (now implemented by partial_function)
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 bulwahn 2010-12-03 explaining quickcheck testers in the documentation
2010-11-28 wenzelm 2010-11-28 Parse.liberal_name for document antiquotations and attributes;
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-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-10-29 wenzelm 2010-10-29 eliminated obsolete \_ escapes in rail environments;