2001-10-04 wenzelm 2001-10-04 updated;
2001-10-04 berghofe 2001-10-04 Fixed bug in decompose.
2001-10-03 wenzelm 2001-10-03 Tools/induct_attrib.ML now part of Pure;
2001-10-03 wenzelm 2001-10-03 Isar/induct_attrib.ML;
2001-10-03 wenzelm 2001-10-03 *** empty log message ***
2001-10-03 wenzelm 2001-10-03 moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
2001-10-03 wenzelm 2001-10-03 tuned parentheses in relational expressions;
2001-10-03 wenzelm 2001-10-03 moved linorder_cases to theory Ord;
2001-10-03 wenzelm 2001-10-03 linorder_cases supersedes linorder_less_split; tuned parentheses in relational expressions;
2001-10-03 paulson 2001-10-03 eta-expansion required for SML/NJ
2001-10-02 wenzelm 2001-10-02 support non-oriented infix;
2001-10-01 wenzelm 2001-10-01 tuned;
2001-10-01 wenzelm 2001-10-01 tuned;
2001-10-01 wenzelm 2001-10-01 *** empty log message ***
2001-10-01 wenzelm 2001-10-01 initial setup for chapter on document preparation;
2001-10-01 wenzelm 2001-10-01 updated output;
2001-10-01 streckem 2001-10-01 - declared wf_java_prog as syntax (previously: definition) - in wf_java_mdecl: added preconditions for 'This' - rule LAss: precondition v ~=This
2001-10-01 streckem 2001-10-01 Removed some unfoldings of defs after declaring wf_java_prog as syntax
2001-10-01 streckem 2001-10-01 Added axiom e~=This to reflect strengthened precond. in rule LAss
2001-10-01 streckem 2001-10-01 Minor modifications
2001-10-01 wenzelm 2001-10-01 added Ordinals example;
2001-09-30 berghofe 2001-09-30 Tuned indentation of abstractions.
2001-09-28 wenzelm 2001-09-28 tuned;
2001-09-28 wenzelm 2001-09-28 inductive: no collective atts;
2001-09-28 wenzelm 2001-09-28 inductive: no collective atts;
2001-09-28 wenzelm 2001-09-28 oops;
2001-09-28 wenzelm 2001-09-28 tuned;
2001-09-28 wenzelm 2001-09-28 recdef (permissive); inductive: no collective atts;
2001-09-28 wenzelm 2001-09-28 *** empty log message ***
2001-09-28 wenzelm 2001-09-28 prove: ``strict'' argument;
2001-09-28 wenzelm 2001-09-28 internal thm numbering with ":" instead of "_";
2001-09-28 wenzelm 2001-09-28 avoid handle _;
2001-09-28 wenzelm 2001-09-28 permissive option;
2001-09-28 wenzelm 2001-09-28 inductive: no collective atts;
2001-09-28 wenzelm 2001-09-28 updated;
2001-09-28 wenzelm 2001-09-28 recdef (permissive);
2001-09-28 berghofe 2001-09-28 Tuned section about parsing and printing proof terms.
2001-09-28 berghofe 2001-09-28 mksimps and mk_eq_True no longer raise THM exception.
2001-09-28 berghofe 2001-09-28 Added label for section on terms.
2001-09-28 berghofe 2001-09-28 Added documentation for proof terms.
2001-09-28 berghofe 2001-09-28 Added TYPE to Pure grammar.
2001-09-28 berghofe 2001-09-28 Added \ttlbrack and \ttrbrack.
2001-09-28 berghofe 2001-09-28 Added TPHOLs2000 paper about proof terms.
2001-09-28 wenzelm 2001-09-28 updated;
2001-09-28 wenzelm 2001-09-28 tuned;
2001-09-28 wenzelm 2001-09-28 tuned;
2001-09-28 berghofe 2001-09-28 - Exchanged % and %%. - Fixed bug in shrink.
2001-09-28 berghofe 2001-09-28 - Tuned syntax - proof_of_term: fixed problems with dummy patterns and typing information
2001-09-28 berghofe 2001-09-28 - Exchanged % and %% - Renamed reconstruct_prf to reconstruct_proof
2001-09-28 berghofe 2001-09-28 Exchanged % and %%.
2001-09-27 wenzelm 2001-09-27 HOL: eliminated global items;
2001-09-27 wenzelm 2001-09-27 updated;
2001-09-27 wenzelm 2001-09-27 eliminated theories "equalities" and "mono" (made part of "Typedef", which supercedes "subset");
2001-09-27 wenzelm 2001-09-27 renamed theory "subset" to "Typedef";
2001-09-27 wenzelm 2001-09-27 unsymbolize;
2001-09-27 wenzelm 2001-09-27 renamed "()" to Unity;
2001-09-27 wenzelm 2001-09-27 HOLogic.unit;
2001-09-27 wenzelm 2001-09-27 made unit type local;
2001-09-27 wenzelm 2001-09-27 tuned:
2001-09-27 wenzelm 2001-09-27 renamed "()" to Unity, made local;