src/HOL/Metis_Examples/Big_O.thy
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