src/HOL/ex/Recdefs.thy
2005-06-17 haftmann 2005-06-17 migrated theory headers to new format
2004-06-16 paulson 2004-06-16 new fib example
2003-10-22 paulson 2003-10-22 InductiveInvariant_examples illustrates advanced recursive function definitions
2001-11-03 wenzelm 2001-11-03 tuned;
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-09-28 wenzelm 2001-09-28 recdef (permissive);
2001-02-01 wenzelm 2001-02-01 converted to new-style theories;
2000-03-20 paulson 2000-03-20 deleted unnecessary "simpset" part from recdef
2000-03-10 paulson 2000-03-10 tidied
1999-04-22 wenzelm 1999-04-22 recdef requires theory Recdef;
1999-04-20 paulson 1999-04-20 Main is the correct parent
1998-09-18 paulson 1998-09-18 new theorem less_Suc_eq_le
1998-07-03 wenzelm 1998-07-03 stepping stones: Recdef, Main; String now part of main HOL;