src/HOL/NSA/HyperDef.thy
2012-03-25 huffman 2012-03-25 merged fork with new numeral representation (see NEWS)
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'
2011-06-29 wenzelm 2011-06-29 modernized some simproc setup;
2011-04-23 wenzelm 2011-04-23 modernized specifications;
2010-08-25 wenzelm 2010-08-25 renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;
2010-07-12 haftmann 2010-07-12 dropped superfluous [code del]s
2010-04-26 haftmann 2010-04-26 use new classes (linordered_)field_inverse_zero
2010-04-26 haftmann 2010-04-26 dropped group_simps, ring_simps, field_eq_simps
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-05 haftmann 2010-02-05 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
2009-05-11 haftmann 2009-05-11 qualified names for Lin_Arith tactics and simprocs
2009-05-11 haftmann 2009-05-11 tuned interface of Lin_Arith
2009-04-28 haftmann 2009-04-28 stripped class recpower further
2009-04-27 haftmann 2009-04-27 cleaned up theory power further
2009-04-23 haftmann 2009-04-23 adaptions due to rearrangment of power operation
2009-03-04 huffman 2009-03-04 declare power_Suc [simp]; remove redundant type-specific versions of power_Suc
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-11 huffman 2008-07-11 instance real_field < field_char_0; instance star :: (field_char_0) field_char_0
2008-07-03 huffman 2008-07-03 move nonstandard analysis theories to NSA directory