src/HOL/NSA/StarDef.thy
2015-03-23 haftmann 2015-03-23 distributivity of partial minus establishes desired properties of dvd in semirings
2015-03-23 haftmann 2015-03-23 explicit commutative additive inverse operation; more explicit focal point for commutative monoids with an inverse operation
2015-03-12 Andreas Lochbihler 2015-03-12 make proofs work with 4762c690a75c
2015-03-10 Andreas Lochbihler 2015-03-10 more type class instances
2015-02-19 haftmann 2015-02-19 establish unique preferred fact names
2014-11-02 wenzelm 2014-11-02 modernized header;
2014-10-29 wenzelm 2014-10-29 modernized setup;
2014-07-04 haftmann 2014-07-04 reduced name variants for assoc and commute on plus and mult
2014-03-22 wenzelm 2014-03-22 more antiquotations;
2014-03-04 huffman 2014-03-04 remove simp rules made redundant by the replacement of neg_numeral with negated numerals
2013-11-25 traytel 2013-11-25 adapt to 9733ab5c1df6
2013-11-19 haftmann 2013-11-19 eliminiated neg_numeral in favour of - (numeral _)
2013-11-01 haftmann 2013-11-01 more simplification rules on unary and binary minus
2012-10-19 webertj 2012-10-19 Renamed {left,right}_distrib to distrib_{right,left}.
2012-10-12 wenzelm 2012-10-12 discontinued obsolete typedef (open) syntax;
2012-08-22 wenzelm 2012-08-22 prefer ML_file over old uses;
2012-04-12 wenzelm 2012-04-12 more standard method setup;
2012-04-04 huffman 2012-04-04 rename ML structure to avoid shadowing earlier name
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