src/HOL/Isar_examples/Fibonacci.thy
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;