src/HOL/NSA/StarDef.thy
2012-03-25 huffman 2012-03-25 merged fork with new numeral representation (see NEWS)
2011-12-28 wenzelm 2011-12-28 reverted some changes for set->predicate transition, according to "hg log -u berghofe -r Isabelle2007:Isabelle2008"; tuned proofs;
2011-11-30 wenzelm 2011-11-30 prefer typedef without extra definition and alternative name; tuned proofs;
2011-11-20 wenzelm 2011-11-20 eliminated obsolete "standard";
2011-11-17 huffman 2011-11-17 HOL-NSA: add number_semiring instance, reformulate several lemmas using '2' instead of '1+1'
2010-11-29 haftmann 2010-11-29 equivI has replaced equiv.intro
2010-09-13 nipkow 2010-09-13 renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
2010-09-07 nipkow 2010-09-07 expand_fun_eq -> ext_iff expand_set_eq -> set_ext_iff Naming in line now with multisets
2010-08-23 haftmann 2010-08-23 dropped type classes mult_mono and mult_mono1; tuned names of technical rule duplicates
2010-08-20 haftmann 2010-08-20 more concise characterization of of_nat operation and class semiring_char_0
2010-07-12 haftmann 2010-07-12 dropped superfluous [code del]s
2010-04-27 haftmann 2010-04-27 tuned class linordered_field_inverse_zero
2010-04-27 haftmann 2010-04-27 instances for *_inverse_zero classes
2010-04-26 haftmann 2010-04-26 class division_ring_inverse_zero
2010-02-10 haftmann 2010-02-10 division ring assumes divide_inverse
2010-02-08 haftmann 2010-02-08 renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
2010-02-08 haftmann 2010-02-08 dropped accidental duplication of "lin" prefix from cs. 108662d50512
2010-02-08 haftmann 2010-02-08 dropped instantiations for combined lattices
2010-02-05 haftmann 2010-02-05 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
2009-04-29 haftmann 2009-04-29 farewell to class recpower
2009-04-23 haftmann 2009-04-23 adaptions due to rearrangment of power operation
2009-03-26 wenzelm 2009-03-26 interpretation/interpret: prefixes are mandatory by default;
2009-03-02 nipkow 2009-03-02 name changes
2009-02-13 huffman 2009-02-13 add class cancel_comm_monoid_add
2008-12-15 ballarin 2008-12-15 More porting to new locales.
2008-10-10 haftmann 2008-10-10 `code func` now just `code`
2008-08-29 haftmann 2008-08-29 fixed names of class assumptions
2008-07-25 haftmann 2008-07-25 added class preorder
2008-07-18 haftmann 2008-07-18 moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
2008-07-03 huffman 2008-07-03 move nonstandard analysis theories to NSA directory