src/HOL/Real/Hyperreal/HyperDef.ML
2000-06-22 wenzelm 2000-06-22 bind_thm(s);
2000-06-14 paulson 2000-06-14 tidied
2000-06-07 paulson 2000-06-07 replacing 0hr by (0::hypreal)
2000-06-07 paulson 2000-06-07 First round of changes, towards installation of simprocs * replacing 0r by (0::real0 * better rewriting, especially pulling out signs in (-x)*y = - (x*y), etc.
2000-06-01 fleuriot 2000-06-01 Updated files to remove 0r and 1r from theorems in descendant theories of RealBin. Some new theorems added.
2000-05-10 wenzelm 2000-05-10 fixed theory deps;
1999-10-11 paulson 1999-10-11 replaced {x. True} by UNIV to work with the new simprule, Collect_const
1999-09-07 wenzelm 1999-09-07 isatool expandshort;
1999-08-23 wenzelm 1999-08-23 isatool expandshort;
1999-08-16 paulson 1999-08-16 new theory Real/Hyperreal/HyperDef and file fuf.ML