src/ZF/ArithSimp.thy
2012-08-22 ago prefer ML_file over old uses;
2012-03-06 ago Using mathematical notation for <-> and cardinal arithmetic
2012-03-06 ago mathematical symbols instead of ASCII
2011-02-18 ago more precise headers;
2010-03-13 ago removed old CVS Ids;
2007-10-07 ago modernized specifications;
2005-06-17 ago migrated theory headers to new format
2005-02-01 ago the new subst tactic, by Lucas Dixon
2003-06-20 ago Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
2003-06-02 ago Further tweaks of ZF/UNITY
2003-05-27 ago updating ZF-UNITY with Sidi's new material
2003-01-23 ago tidying (by script)
2002-10-01 ago Numerous cosmetic changes, prompted by the new simplifier
2002-09-30 ago Adapted to new simplifier.
2002-07-14 ago improved presentation markup
2002-07-09 ago better document preparation
2002-06-29 ago conversion of many files to Isar format
2000-08-07 ago instantiated Cancel_Numerals for "nat" in ZF