Sun, 21 Dec 2003 08:27:44 +0100 removed insert_Diff_single from simpset because it interfered with Auth :-(
nipkow [Sun, 21 Dec 2003 08:27:44 +0100] rev 14306
removed insert_Diff_single from simpset because it interfered with Auth :-(
Fri, 19 Dec 2003 17:13:28 +0100 tidying first part of HyperArith0.ML, using generic lemmas
paulson [Fri, 19 Dec 2003 17:13:28 +0100] rev 14305
tidying first part of HyperArith0.ML, using generic lemmas
Fri, 19 Dec 2003 10:38:48 +0100 minor tweaks
paulson [Fri, 19 Dec 2003 10:38:48 +0100] rev 14304
minor tweaks
Fri, 19 Dec 2003 10:38:39 +0100 type hypreal is an ordered field
paulson [Fri, 19 Dec 2003 10:38:39 +0100] rev 14303
type hypreal is an ordered field
Fri, 19 Dec 2003 04:28:45 +0100 *** empty log message ***
nipkow [Fri, 19 Dec 2003 04:28:45 +0100] rev 14302
*** empty log message ***
Thu, 18 Dec 2003 15:06:24 +0100 tidied
paulson [Thu, 18 Dec 2003 15:06:24 +0100] rev 14301
tidied
Thu, 18 Dec 2003 08:20:36 +0100 *** empty log message ***
nipkow [Thu, 18 Dec 2003 08:20:36 +0100] rev 14300
*** empty log message ***
Wed, 17 Dec 2003 16:23:52 +0100 converted Hyperreal/HyperDef to Isar script
paulson [Wed, 17 Dec 2003 16:23:52 +0100] rev 14299
converted Hyperreal/HyperDef to Isar script
Tue, 16 Dec 2003 23:24:17 +0100 fixed PG link
kleing [Tue, 16 Dec 2003 23:24:17 +0100] rev 14298
fixed PG link
Tue, 16 Dec 2003 15:38:09 +0100 converted Hyperreal/HyperOrd to new-style theory
paulson [Tue, 16 Dec 2003 15:38:09 +0100] rev 14297
converted Hyperreal/HyperOrd to new-style theory
(0) -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip