src/HOL/NSA/NSA.thy
2015-11-13 paulson 2015-11-13 Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
2015-11-10 paulson 2015-11-10 Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
2015-10-09 wenzelm 2015-10-09 discontinued specific HTML syntax;
2015-09-30 paulson 2015-09-30 real_of_nat_Suc is now a simprule
2015-09-01 wenzelm 2015-09-01 eliminated \<Colon>;
2015-08-31 wenzelm 2015-08-31 prefer symbols;
2015-04-12 hoelzl 2015-04-12 replace Filters in NSA by HOL-Filters
2015-03-31 haftmann 2015-03-31 given up separate type classes demanding `inverse 0 = 0`
2015-03-04 wenzelm 2015-03-04 tuned signature -- prefer qualified names;
2014-11-02 wenzelm 2014-11-02 modernized header;
2014-10-29 wenzelm 2014-10-29 more standard theory name;
2014-07-05 haftmann 2014-07-05 prefer ac_simps collections over separate name bindings for add and mult
2014-07-04 haftmann 2014-07-04 reduced name variants for assoc and commute on plus and mult
2014-04-12 nipkow 2014-04-12 made mult_pos_pos a simp rule
2014-04-11 nipkow 2014-04-11 made divide_pos_pos a simp rule
2014-03-20 paulson 2014-03-20 fixing messy proofs
2014-03-19 paulson 2014-03-19 Some rationalisation of basic lemmas
2013-11-19 haftmann 2013-11-19 eliminiated neg_numeral in favour of - (numeral _)
2013-11-05 hoelzl 2013-11-05 move Lubs from HOL to HOL-Library (replaced by conditionally complete lattices)
2013-11-01 haftmann 2013-11-01 more simplification rules on unary and binary minus
2013-03-26 hoelzl 2013-03-26 merge RComplete into RealDef
2012-03-25 huffman 2012-03-25 merged fork with new numeral representation (see NEWS)
2011-11-17 huffman 2011-11-17 simplify implementation of approx_reorient_simproc
2011-11-17 huffman 2011-11-17 name simp theorems st_0 and st_1
2011-09-17 haftmann 2011-09-17 tuned
2011-01-13 wenzelm 2011-01-13 eliminated global prems; tuned proofs;
2010-09-06 wenzelm 2010-09-06 more antiquotations;
2010-07-19 haftmann 2010-07-19 diff_minus subsumes diff_def
2010-07-12 haftmann 2010-07-12 dropped superfluous [code del]s
2010-05-09 huffman 2010-05-09 real_mult_commute -> mult_commute
2010-04-26 haftmann 2010-04-26 use new classes (linordered_)field_inverse_zero
2010-04-26 haftmann 2010-04-26 class division_ring_inverse_zero
2010-02-19 haftmann 2010-02-19 moved remaning class operations from Algebras.thy to Groups.thy
2010-01-28 haftmann 2010-01-28 new theory Algebras.thy for generic algebraic structures
2009-12-18 huffman 2009-12-18 rename equals_zero_I to minus_unique (keep old name too)
2009-10-17 wenzelm 2009-10-17 eliminated hard tabulators, guessing at each author's individual tab-width; tuned headers;
2009-07-23 wenzelm 2009-07-23 more @{theory} antiquotations;
2009-06-05 huffman 2009-06-05 fix type of hnorm
2009-04-28 haftmann 2009-04-28 stripped class recpower further
2009-03-12 haftmann 2009-03-12 vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
2009-02-24 huffman 2009-02-24 fix lemma hypreal_hnorm_def
2008-12-03 haftmann 2008-12-03 made repository layout more coherent with logical distribution structure; stripped some $Id$s
2008-10-10 haftmann 2008-10-10 `code func` now just `code`
2008-07-03 huffman 2008-07-03 move nonstandard analysis theories to NSA directory