src/HOL/Real/Hyperreal/HyperDef.ML
Thu, 21 Dec 2000 18:08:10 +0100 paulson further tidying of NSA proofs
Thu, 21 Dec 2000 10:16:33 +0100 paulson more tidying, especially to rationalize the simprules
Wed, 20 Dec 2000 12:15:52 +0100 paulson further tidying
Mon, 18 Dec 2000 12:23:54 +0100 paulson tidying and adding new proofs
Fri, 15 Dec 2000 17:41:38 +0100 paulson further round of tidying
Tue, 12 Dec 2000 12:01:19 +0100 paulson first stage in tidying up Real and Hyperreal.
Wed, 06 Dec 2000 12:34:40 +0100 bauerg converted rinv and hrinv to inverse;
Thu, 21 Sep 2000 12:11:38 +0200 fleuriot Updated Files with new theorems
Fri, 15 Sep 2000 12:39:57 +0200 paulson renamed (most of...) the select rules
Tue, 25 Jul 2000 00:00:22 +0200 wenzelm avoid referencing thy value;
Wed, 19 Jul 2000 12:33:19 +0200 paulson changed / to // for quotienting; general tidying
Tue, 18 Jul 2000 21:44:42 +0200 wenzelm addsplits [split_if];
Tue, 18 Jul 2000 21:08:57 +0200 wenzelm removed obsolete expand_if = split_if;
Thu, 22 Jun 2000 23:04:34 +0200 wenzelm bind_thm(s);
Wed, 14 Jun 2000 18:24:41 +0200 paulson tidied
Wed, 07 Jun 2000 17:14:58 +0200 paulson replacing 0hr by (0::hypreal)
Wed, 07 Jun 2000 12:14:18 +0200 paulson First round of changes, towards installation of simprocs
Thu, 01 Jun 2000 11:22:27 +0200 fleuriot Updated files to remove 0r and 1r from theorems in descendant theories
Wed, 10 May 2000 22:34:30 +0200 wenzelm fixed theory deps;
Mon, 11 Oct 1999 10:52:51 +0200 paulson replaced {x. True} by UNIV to work with the new simprule, Collect_const
Tue, 07 Sep 1999 10:40:58 +0200 wenzelm isatool expandshort;
Mon, 23 Aug 1999 15:30:26 +0200 wenzelm isatool expandshort;
Mon, 16 Aug 1999 18:41:06 +0200 paulson new theory Real/Hyperreal/HyperDef and file fuf.ML
less more (0) tip