src/HOL/W0/W0.thy
2008-03-20 haftmann 2008-03-20 tuned proofs
2008-03-19 wenzelm 2008-03-19 more antiquotations;
2007-09-27 paulson 2007-09-27 removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering theorems of Nat.thy are hidden by the Ordering.thy versions
2007-07-20 haftmann 2007-07-20 dropped Nat.ML legacy bindings
2007-07-11 berghofe 2007-07-11 Adapted to new inductive definition package.
2007-06-13 wenzelm 2007-06-13 tuned proofs: avoid implicit prems;
2007-03-29 haftmann 2007-03-29 dropped legacy ML bindings
2006-12-06 wenzelm 2006-12-06 removed legacy ML bindings;
2006-11-17 wenzelm 2006-11-17 more robust syntax for definition/abbreviation/notation;
2006-09-13 krauss 2006-09-13 Major update to function package, including new syntax and the (only theoretical) ability to handle local contexts.
2006-09-11 wenzelm 2006-09-11 induct method: renamed 'fixing' to 'arbitrary';
2006-05-29 wenzelm 2006-05-29 tuned;
2006-05-27 wenzelm 2006-05-27 tuned;
2006-04-09 wenzelm 2006-04-09 tuned syntax/abbreviations;
2004-10-11 nipkow 2004-10-11 Proofs needed to be updated because induction now preserves name of induction variable.
2004-08-18 nipkow 2004-08-18 import -> imports
2004-06-21 kleing 2004-06-21 Merged in license change from Isabelle2004
2003-04-01 nipkow 2003-04-01 Made empty a translation rather than a constant.
2002-09-30 berghofe 2002-09-30 Adapted to new simplifier.
2002-08-27 wenzelm 2002-08-27 avoid duplicate fact bindings;
2002-02-26 wenzelm 2002-02-26 tuned;
2002-02-26 wenzelm 2002-02-26 tuned;
2002-02-26 wenzelm 2002-02-26 converted;