src/HOL/ex/Sqrt.thy
2016-02-17 haftmann 2016-02-17 dropped various legacy fact bindings
2015-12-01 paulson 2015-12-01 Removal of redundant lemmas (diff_less_iff, diff_le_iff) and of the abbreviation Exp. Addition of some new material.
2015-11-13 paulson 2015-11-13 Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
2015-07-08 haftmann 2015-07-08 tuned facts
2014-11-22 wenzelm 2014-11-22 misc tuning and modernization;
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
2014-07-05 haftmann 2014-07-05 prefer ac_simps collections over separate name bindings for add and mult
2013-09-12 huffman 2013-09-12 remove unneeded assumption from prime_dvd_power lemmas; add iff forms of prime_dvd_power lemmas (thanks to Jason Dagit)
2013-08-13 wenzelm 2013-08-13 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
2013-04-15 hoelzl 2013-04-15 use automatic type coerctions in Sqrt example
2012-02-15 wenzelm 2012-02-15 uniform Isar source formatting for this file;
2011-12-19 nipkow 2011-12-19 added old chestnut
2009-09-01 haftmann 2009-09-01 some reorganization of number theory
2009-07-07 nipkow 2009-07-07 renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
2009-06-18 huffman 2009-06-18 update ex/Sqrt.thy to use new GCD library
2009-03-10 wenzelm 2009-03-10 tuned proofs; tuned document;
2008-12-03 haftmann 2008-12-03 made repository layout more coherent with logical distribution structure; stripped some $Id$s