src/HOL/Isar_examples/Fibonacci.thy
2005-11-23 wenzelm 2005-11-23 tuned induction proofs;
2005-11-10 wenzelm 2005-11-10 tuned proofs;
2005-06-17 haftmann 2005-06-17 migrated theory headers to new format
2005-01-14 nipkow 2005-01-14 made diff_less a simp rule
2001-10-16 wenzelm 2001-10-16 tuned induction proofs;
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'.
2000-11-06 wenzelm 2000-11-06 improved: 'induct' handle non-atomic goals;
2000-09-17 wenzelm 2000-09-17 isar-strip-terminators;
2000-09-06 nipkow 2000-09-06 less_induct -> nat_less_induct
2000-09-04 paulson 2000-09-04 minor fixes for new version of Primes.thy
2000-08-19 wenzelm 2000-08-19 tuned;
2000-05-23 paulson 2000-05-23 added type constraint ::nat because 0 is now overloaded
2000-05-05 wenzelm 2000-05-05 adapted to new arithmetic simprocs;
2000-03-30 nipkow 2000-03-30 recdef.rules -> recdef.simps
2000-02-27 wenzelm 2000-02-27 even better induct setup;
2000-02-22 wenzelm 2000-02-22 tuned "induct" syntax;
1999-12-07 wenzelm 1999-12-07 tuned;
1999-12-07 wenzelm 1999-12-07 tuned;