src/HOL/Metis_Examples/Big_O.thy
2015-12-28 wenzelm 2015-12-28 more symbols;
2015-12-28 wenzelm 2015-12-28 more symbols;
2015-12-10 paulson 2015-12-10 not_leE -> not_le_imp_less and other tidying
2015-09-01 wenzelm 2015-09-01 eliminated \<Colon>;
2015-03-31 haftmann 2015-03-31 given up separate type classes demanding `inverse 0 = 0`
2015-02-19 haftmann 2015-02-19 establish unique preferred fact names
2015-02-18 haftmann 2015-02-18 inlined rules to free user-space from technical names
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
2014-07-04 haftmann 2014-07-04 reduced name variants for assoc and commute on plus and mult
2014-06-28 haftmann 2014-06-28 fact consolidation
2014-06-12 blanchet 2014-06-12 renamed Sledgehammer options
2014-04-11 nipkow 2014-04-11 made mult_nonneg_nonneg a simp rule
2014-01-30 blanchet 2014-01-30 renamed Sledgehammer options for symmetry between positive and negative versions
2013-12-25 haftmann 2013-12-25 prefer more canonical names for lemmas on min/max
2013-11-01 haftmann 2013-11-01 more simplification rules on unary and binary minus
2013-08-13 wenzelm 2013-08-13 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
2013-02-14 smolkas 2013-02-14 renamed sledgehammer_shrink to sledgehammer_compress
2012-11-06 blanchet 2012-11-06 renamed Sledgehammer option
2012-10-18 blanchet 2012-10-18 renamed Isar-proof related options + changed semantics of Isar shrinking
2012-04-12 krauss 2012-04-12 Set_Algebras: removed syntax \<oplus> and \<otimes>, in favour of plain + and *
2012-03-25 huffman 2012-03-25 merged fork with new numeral representation (see NEWS)
2012-02-24 blanchet 2012-02-24 rephrase some slow "metis" calls
2012-01-30 blanchet 2012-01-30 example tuning
2012-01-30 blanchet 2012-01-30 example tuning
2011-12-01 blanchet 2011-12-01 tuning
2011-11-18 blanchet 2011-11-18 more "metis" calls in example
2011-11-17 huffman 2011-11-17 Int.thy: remove duplicate lemmas double_less_0_iff and odd_less_0, use {even,odd}_less_0_iff instead
2011-11-15 huffman 2011-11-15 Metis_Examples/Big_O.thy: add number_ring class constraints, adapt proofs to use cancellation simprocs
2011-10-27 huffman 2011-10-27 fix bug in cancel_factor simprocs so they will work on goals like 'x * y < x * z' where the common term is already on the left
2011-06-06 blanchet 2011-06-06 tuned Metis examples