paulson [Tue, 23 Dec 2003 14:46:08 +0100] rev 14321
 
new theorems
paulson [Tue, 23 Dec 2003 14:45:47 +0100] rev 14320
 
tidying up hcomplex arithmetic
paulson [Tue, 23 Dec 2003 14:45:23 +0100] rev 14319
 
renaming some theorems
paulson [Tue, 23 Dec 2003 12:54:45 +0100] rev 14318
 
type hcomplex is now in class field
paulson [Tue, 23 Dec 2003 12:54:15 +0100] rev 14317
 
more ML bindings
kleing [Tue, 23 Dec 2003 06:35:41 +0100] rev 14316
 
added some [intro?] and [trans] for list_all2 lemmas
nipkow [Mon, 22 Dec 2003 22:52:38 +0100] rev 14315
 
Updated proofs due to changes in Set.thy.
paulson [Mon, 22 Dec 2003 18:29:20 +0100] rev 14314
 
converted Complex/NSComplex to Isar script
paulson [Mon, 22 Dec 2003 16:22:14 +0100] rev 14313
 
removal of the abel_cancel simproc for hypreal
paulson [Mon, 22 Dec 2003 15:42:21 +0100] rev 14312
 
downgrading abel_cancel
paulson [Mon, 22 Dec 2003 15:41:25 +0100] rev 14311
 
new binding
paulson [Mon, 22 Dec 2003 14:12:54 +0100] rev 14310
 
simplifying
paulson [Mon, 22 Dec 2003 12:50:22 +0100] rev 14309
 
moving HyperArith0.ML to other theories
paulson [Mon, 22 Dec 2003 12:50:01 +0100] rev 14308
 
removing obsolete bindings
paulson [Sun, 21 Dec 2003 18:39:27 +0100] rev 14307
 
tidying of HOL/Auth esp Guard lemmas
nipkow [Sun, 21 Dec 2003 08:27:44 +0100] rev 14306
 
removed insert_Diff_single from simpset because it interfered with Auth :-(
paulson [Fri, 19 Dec 2003 17:13:28 +0100] rev 14305
 
tidying first part of HyperArith0.ML, using generic lemmas
paulson [Fri, 19 Dec 2003 10:38:48 +0100] rev 14304
 
minor tweaks
paulson [Fri, 19 Dec 2003 10:38:39 +0100] rev 14303
 
type hypreal is an ordered field
nipkow [Fri, 19 Dec 2003 04:28:45 +0100] rev 14302
 
*** empty log message ***
paulson [Thu, 18 Dec 2003 15:06:24 +0100] rev 14301
 
tidied
nipkow [Thu, 18 Dec 2003 08:20:36 +0100] rev 14300
 
*** empty log message ***
paulson [Wed, 17 Dec 2003 16:23:52 +0100] rev 14299
 
converted Hyperreal/HyperDef to Isar script
kleing [Tue, 16 Dec 2003 23:24:17 +0100] rev 14298
 
fixed PG link
paulson [Tue, 16 Dec 2003 15:38:09 +0100] rev 14297
 
converted Hyperreal/HyperOrd to new-style theory
paulson [Mon, 15 Dec 2003 17:08:41 +0100] rev 14296
 
updated references to the now-pornographic proofgeneral.org
paulson [Mon, 15 Dec 2003 16:38:25 +0100] rev 14295
 
more general lemmas for Ring_and_Field
paulson [Sat, 13 Dec 2003 09:33:52 +0100] rev 14294
 
absolute value theorems moved to HOL/Ring_and_Field
paulson [Fri, 12 Dec 2003 15:05:18 +0100] rev 14293
 
moving some division theorems to Ring_and_Field
kleing [Fri, 12 Dec 2003 03:41:47 +0100] rev 14292
 
changed proof general links