doc-src/IsarRef/Thy/HOL_Specific.thy
2010-10-29 wenzelm 2010-10-29 proper markup of formal text;
2010-10-29 bulwahn 2010-10-29 updating documentation on quickcheck in the Isar reference
2010-10-26 krauss 2010-10-26 basic documentation for command partial_function
2010-10-26 krauss 2010-10-26 remove outdated "(otherwise)" syntax from manual
2010-09-22 haftmann 2010-09-22 formal syntax diagram for code_reflect
2010-08-27 haftmann 2010-08-27 official support for Scala
2010-08-17 haftmann 2010-08-17 formally document `code abstype` and `code abstract` attributes
2010-07-14 haftmann 2010-07-14 export_code without file prints to standard output
2010-07-08 haftmann 2010-07-08 updated documentation
2010-06-17 haftmann 2010-06-17 added simp evaluator
2010-06-14 haftmann 2010-06-14 tuned internal order
2010-06-14 haftmann 2010-06-14 corrected syntax diagram
2010-04-28 wenzelm 2010-04-28 removed material that is out of scope of this manual;
2010-04-15 wenzelm 2010-04-15 HOL record: explicitly allow sort constraints;
2010-04-14 hoelzl 2010-04-14 Spelling error: theroems -> theorems
2010-03-19 wenzelm 2010-03-19 allow sort constraints in HOL/typedef;
2010-03-13 wenzelm 2010-03-13 removed obsolete HOL 'typedecl'; local theory version of HOL 'typedef';
2010-03-06 wenzelm 2010-03-06 eliminated Args.bang_facts (legacy feature);
2010-02-24 wenzelm 2010-02-24 allow general mixfix syntax for type constructors;
2010-02-23 blanchet 2010-02-23 document Quickcheck's "no_assms" option
2009-12-23 haftmann 2009-12-23 updated documentation
2009-11-23 krauss 2009-11-23 documented size_change in isar-ref manual
2009-11-23 krauss 2009-11-23 clarified; checked
2009-07-14 haftmann 2009-07-14 code attributes use common underscore convention
2009-07-02 haftmann 2009-07-02 more friendly wrt. PGs interpretation of compound *); added dedicated section on value and quickcheck
2009-05-26 haftmann 2009-05-26 documented print_codeproc command
2009-04-03 wenzelm 2009-04-03 fixed formal markup;
2009-04-03 nipkow 2009-04-03 Finite_Set: lemma IsarRef: attribute arith
2009-03-04 blanchet 2009-03-04 Merge.
2009-03-04 blanchet 2009-03-04 Merge.
2009-02-28 wenzelm 2009-02-28 added method "coherent"; tuned formal markup;
2009-02-28 wenzelm 2009-02-28 moved method "iprover" to HOL specific part;
2009-01-19 haftmann 2009-01-19 "code equation" replaces "defining equation"
2008-12-15 wenzelm 2008-12-15 repaired railroad accident;
2008-12-15 wenzelm 2008-12-15 added 'atp_messages' command, which displays recent messages synchronously;
2008-11-13 wenzelm 2008-11-13 updated/refined types of Isar language elements, removed special LaTeX macros;
2008-11-13 wenzelm 2008-11-13 unified use of declaration environment with IsarImplementation; tuned ML decls;
2008-11-13 wenzelm 2008-11-13 tuned;
2008-10-24 haftmann 2008-10-24 simplified syntax for class parameters
2008-10-15 wenzelm 2008-10-15 added sledgehammer etc.;
2008-10-10 haftmann 2008-10-10 `code func` now just `code`
2008-07-30 haftmann 2008-07-30 clarified
2008-07-03 haftmann 2008-07-03 adjusted rep_datatype
2008-06-10 wenzelm 2008-06-10 case_tac/induct_tac: use same declarations as cases/induct;
2008-06-10 haftmann 2008-06-10 major refactorings in code generator modules
2008-06-02 wenzelm 2008-06-02 moved (ax_)specification to end;
2008-06-02 wenzelm 2008-06-02 tuned spacing;
2008-05-24 wenzelm 2008-05-24 function: uniform treatment of target, not as config;
2008-05-14 wenzelm 2008-05-14 proper checking of various Isar elements;
2008-05-08 wenzelm 2008-05-08 replaced some latex macros by antiquotations;
2008-05-08 wenzelm 2008-05-08 misc tuning;
2008-05-08 wenzelm 2008-05-08 converted HOL specific elements;
2008-05-07 wenzelm 2008-05-07 added logic-specific sessions;