src/HOL/NatArith.ML
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-07 paulson 2001-08-07 Tweaks for 1 -> 1'
2001-07-25 paulson 2001-07-25 partial restructuring to reduce dependence on Axiom of Choice
2001-06-26 paulson 2001-06-26 gave Greatest_le its proper name
2001-06-09 paulson 2001-06-09 addition of the GREATEST quantifier
2001-01-22 paulson 2001-01-22 deleted several obsolete lemmas from NatArith.ML
2000-10-13 nipkow 2000-10-13 *** empty log message ***