src/HOL/Hyperreal/StarClasses.thy
2007-11-06 haftmann 2007-11-06 removed subclass edge ordered_ring < lordered_ring
2007-10-30 haftmann 2007-10-30 continued localization
2007-10-26 haftmann 2007-10-26 changed order of class parameters
2007-09-27 paulson 2007-09-27 removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering theorems of Nat.thy are hidden by the Ordering.thy versions
2007-09-01 nipkow 2007-09-01 final(?) iteration of sgn saga.
2007-08-09 haftmann 2007-08-09 tuned
2007-07-20 haftmann 2007-07-20 split class abs from class minus
2007-07-03 wenzelm 2007-07-03 rename class dom to ring_1_no_zero_divisors (cf. HOL/Ring_and_Field.thy 1.84 by huffman);
2007-06-06 huffman 2007-06-06 add axclass semiring_char_0 for types where of_nat is injective
2007-05-17 haftmann 2007-05-17 tuned
2007-05-17 huffman 2007-05-17 add classes ring_no_zero_divisors and dom
2007-05-10 huffman 2007-05-10 new axclass ring_char_0 for rings with characteristic 0, used for of_int_eq_iff and related lemmas
2007-03-26 haftmann 2007-03-26 naming tuned
2007-03-16 haftmann 2007-03-16 adjusted to new lattice theory developement in Lattices.thy / FixedPoint.thy
2007-03-09 haftmann 2007-03-09 stepping towards uniform lattice theory development in HOL
2007-03-02 haftmann 2007-03-02 prefix of class interpretation not mandatory any longer
2007-02-14 haftmann 2007-02-14 added class "preorder"
2006-11-07 krauss 2006-11-07 * Added annihilation axioms ("x * 0 = 0") to axclass semiring_0. Richer structures do not inherit from semiring_0 anymore, because anihilation is a theorem there, not an axiom. * Generalized axclass "recpower" to arbitrary monoid, not just commutative semirings.
2006-09-27 huffman 2006-09-27 more lemmas about Standard and star_of
2006-09-27 huffman 2006-09-27 define new constant Standard = range star_of
2006-09-20 wenzelm 2006-09-20 renamed axclass_xxxx axclasses;
2006-09-16 huffman 2006-09-16 int_diff_cases moved to Integ/IntDef.thy
2006-09-14 huffman 2006-09-14 add instance for class division_ring
2005-09-15 huffman 2005-09-15 merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
2005-09-12 huffman 2005-09-12 added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
2005-09-06 huffman 2005-09-06 class instances for nonstandard types