src/HOL/ex/Primrec.thy
2011-01-07 bulwahn 2011-01-07 removing obselete Id comments from HOL/ex theories
2009-12-10 paulson 2009-12-10 streamlined proofs
2008-10-03 wenzelm 2008-10-03 removed spurious ResAtp.set_prover;
2008-07-17 nipkow 2008-07-17 beautified proofs
2008-03-19 wenzelm 2008-03-19 removed redundant Nat.less_irrefl;
2008-02-15 haftmann 2008-02-15 <= and < on nat no longer depend on wellfounded relations
2007-10-23 paulson 2007-10-23 random tidying of proofs
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-09-07 paulson 2007-09-07 tidied the proofs
2007-07-11 berghofe 2007-07-11 renamed inductive2 to inductive.
2007-05-13 nipkow 2007-05-13 Got rid of listsp
2007-02-07 berghofe 2007-02-07 Adapted to new inductive definition package.
2006-11-17 wenzelm 2006-11-17 more robust syntax for definition/abbreviation/notation;
2006-05-27 wenzelm 2006-05-27 tuned;
2006-05-17 wenzelm 2006-05-17 renamed CONST to CONSTANT;
2005-07-06 wenzelm 2005-07-06 fixed antiquotation;
2005-06-28 paulson 2005-06-28 stricter first-order check for meson
2005-06-24 paulson 2005-06-24 meson method taking an argument list
2005-06-17 haftmann 2005-06-17 migrated theory headers to new format
2001-10-06 wenzelm 2001-10-06 * sane numerals (stage 2): plain "num" syntax (removed "#");
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-06 nipkow 2001-08-06 turned translation for 1::nat into def. introduced 1' and replaced most occurrences of 1 by 1'.
2001-02-01 wenzelm 2001-02-01 converted to new-style theories;
2000-04-13 nipkow 2000-04-13 Times -> <*> ** -> <*lex*>
1999-04-22 wenzelm 1999-04-22 recdef requires theory Recdef;
1998-10-21 berghofe 1998-10-21 Changed syntax of inductive.
1998-07-24 berghofe 1998-07-24 Adapted to new datatype package.
1997-06-06 paulson 1997-06-06 Mended the definition of ack(0,n)
1997-05-26 paulson 1997-05-26 New example ported from ZF