src/HOL/Datatype_Universe.thy
2005-09-22 nipkow 2005-09-22 renamed rules to iprover
2005-09-17 wenzelm 2005-09-17 tuned document;
2005-08-16 paulson 2005-08-16 classical rules must have names for ATP integration
2004-12-15 paulson 2004-12-15 removal of archaic Abs/Rep proofs
2004-12-09 paulson 2004-12-09 converted Datatype_Universe to new-style theory
2002-10-10 berghofe 2002-10-10 Removed obsolete function "Funs".
2001-10-05 wenzelm 2001-10-05 sane numerals (stage 1): added generic 1, removed 1' and 2 on nat, "num" syntax (still with "#"), Numeral0, Numeral1;
2001-08-08 paulson 2001-08-08 Hilbert_Choice is needed only in Main itself
2001-07-25 paulson 2001-07-25 partial restructuring to reduce dependence on Axiom of Choice
2001-01-09 nipkow 2001-01-09 `` -> and ``` -> ``
2000-10-13 nipkow 2000-10-13 *** empty log message ***
2000-10-12 nipkow 2000-10-12 *** empty log message ***