doc-src/IsarRef/Thy/HOL_Specific.thy
2009-03-04 ago Merge.
2009-03-04 ago Merge.
2009-02-28 ago added method "coherent";
2009-02-28 ago moved method "iprover" to HOL specific part;
2009-01-19 ago "code equation" replaces "defining equation"
2008-12-15 ago repaired railroad accident;
2008-12-15 ago added 'atp_messages' command, which displays recent messages synchronously;
2008-11-13 ago updated/refined types of Isar language elements, removed special LaTeX macros;
2008-11-13 ago unified use of declaration environment with IsarImplementation;
2008-11-13 ago tuned;
2008-10-24 ago simplified syntax for class parameters
2008-10-15 ago added sledgehammer etc.;
2008-10-10 ago `code func` now just `code`
2008-07-30 ago clarified
2008-07-03 ago adjusted rep_datatype
2008-06-10 ago case_tac/induct_tac: use same declarations as cases/induct;
2008-06-10 ago major refactorings in code generator modules
2008-06-02 ago moved (ax_)specification to end;
2008-06-02 ago tuned spacing;
2008-05-24 ago function: uniform treatment of target, not as config;
2008-05-14 ago proper checking of various Isar elements;
2008-05-08 ago replaced some latex macros by antiquotations;
2008-05-08 ago misc tuning;
2008-05-08 ago converted HOL specific elements;
2008-05-07 ago added logic-specific sessions;