src/HOL/Integ/NatSimprocs.ML
2000-05-30 wenzelm 2000-05-30 cleaned up;
2000-05-23 paulson 2000-05-23 added type constraint ::nat because 0 is now overloaded
2000-05-16 paulson 2000-05-16 new policy to simplify the use of numerals: #0 -> 0 #1 -> 1 #2 + n -> Suc (Suc n) similarly for n + #2
2000-05-12 paulson 2000-05-12 new simprules for nat_case and nat_rec simplify_meta_eq now maps #0 to 0 and #1 to 1 in its result
2000-05-10 paulson 2000-05-10 new default simprule for better compatibility with old setup
2000-05-05 paulson 2000-05-05 simprocs now simplify the RHS of their result
2000-05-04 paulson 2000-05-04 further tidying of integer simprocs
2000-05-03 paulson 2000-05-03 Installation of CombineNumerals for the integers Many bug fixes Removal of AssocFold for addition (nat and int)
2000-05-02 paulson 2000-05-02 now with combine_numerals
2000-04-23 paulson 2000-04-23 bug fixes to new simprocs
2000-04-21 paulson 2000-04-21 new file containing simproc invocations, from NatBin.ML