src/HOL/Hyperreal/StarClasses.thy
Tue, 03 Jul 2007 20:26:08 +0200 wenzelm rename class dom to ring_1_no_zero_divisors (cf. HOL/Ring_and_Field.thy 1.84 by huffman);
Wed, 06 Jun 2007 20:49:04 +0200 huffman add axclass semiring_char_0 for types where of_nat is injective
Thu, 17 May 2007 19:49:16 +0200 haftmann tuned
Thu, 17 May 2007 19:29:39 +0200 huffman add classes ring_no_zero_divisors and dom
Thu, 10 May 2007 02:51:53 +0200 huffman new axclass ring_char_0 for rings with characteristic 0, used for of_int_eq_iff and related lemmas
Mon, 26 Mar 2007 14:53:01 +0200 haftmann naming tuned
Fri, 16 Mar 2007 21:32:08 +0100 haftmann adjusted to new lattice theory developement in Lattices.thy / FixedPoint.thy
Fri, 09 Mar 2007 08:45:50 +0100 haftmann stepping towards uniform lattice theory development in HOL
Fri, 02 Mar 2007 15:43:15 +0100 haftmann prefix of class interpretation not mandatory any longer
Wed, 14 Feb 2007 10:06:12 +0100 haftmann added class "preorder"
Tue, 07 Nov 2006 09:33:47 +0100 krauss * Added annihilation axioms ("x * 0 = 0") to axclass semiring_0.
Wed, 27 Sep 2006 01:18:35 +0200 huffman more lemmas about Standard and star_of
Wed, 27 Sep 2006 00:54:10 +0200 huffman define new constant Standard = range star_of
Wed, 20 Sep 2006 00:24:24 +0200 wenzelm renamed axclass_xxxx axclasses;
Sat, 16 Sep 2006 18:04:14 +0200 huffman int_diff_cases moved to Integ/IntDef.thy
Thu, 14 Sep 2006 21:36:26 +0200 huffman add instance for class division_ring
Thu, 15 Sep 2005 23:46:22 +0200 huffman merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
Mon, 12 Sep 2005 23:14:41 +0200 huffman added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
Tue, 06 Sep 2005 23:11:46 +0200 huffman class instances for nonstandard types
less more (0) tip