src/HOL/NSA/HyperDef.thy
2012-03-25 ago merged fork with new numeral representation (see NEWS)
2011-11-20 ago eliminated obsolete "standard";
2011-11-17 ago HOL-NSA: add number_semiring instance, reformulate several lemmas using '2' instead of '1+1'
2011-06-29 ago modernized some simproc setup;
2011-04-23 ago modernized specifications;
2010-08-25 ago renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;
2010-07-12 ago dropped superfluous [code del]s
2010-04-26 ago use new classes (linordered_)field_inverse_zero
2010-04-26 ago dropped group_simps, ring_simps, field_eq_simps
2010-02-08 ago renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
2010-02-08 ago dropped accidental duplication of "lin" prefix from cs. 108662d50512
2010-02-05 ago more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
2009-05-11 ago qualified names for Lin_Arith tactics and simprocs
2009-05-11 ago tuned interface of Lin_Arith
2009-04-28 ago stripped class recpower further
2009-04-27 ago cleaned up theory power further
2009-04-23 ago adaptions due to rearrangment of power operation
2009-03-04 ago declare power_Suc [simp]; remove redundant type-specific versions of power_Suc
2008-12-03 ago made repository layout more coherent with logical distribution structure; stripped some $Id$s
2008-10-10 ago `code func` now just `code`
2008-07-11 ago instance real_field < field_char_0;
2008-07-03 ago move nonstandard analysis theories to NSA directory