src/HOL/ex/Primes.thy
2000-09-12 wenzelm 2000-09-12 renamed atts: rulify to rule_format, elimify to elim_format;
2000-09-11 paulson 2000-09-11 tidied
2000-09-07 wenzelm 2000-09-07 updated attribute names;
2000-09-05 paulson 2000-09-05 tidied, proving gcd_greatest_iff and using induct_tac
2000-09-04 paulson 2000-09-04 Converting HOL/ex/Primes.thy to new style, removing Primes.ML
2000-04-13 nipkow 2000-04-13 made mod_less_divisor a simplification rule.
1999-04-20 paulson 1999-04-20 Main is the correct parent
1998-07-24 berghofe 1998-07-24 Adapted to new datatype package.
1997-07-04 paulson 1997-07-04 New comments on how to deal with unproved termination conditions
1997-05-30 paulson 1997-05-30 Now "primes" is a set
1997-05-20 paulson 1997-05-20 Renamed egcd and gcd; defined the gcd function using TFL
1996-06-14 paulson 1996-06-14 New example of greatest common divisor