src/HOL/MetisExamples/BigO.thy
2007-11-06 haftmann 2007-11-06 removed subclass edge ordered_ring < lordered_ring
2007-10-18 paulson 2007-10-18 some more metis calls
2007-10-18 haftmann 2007-10-18 tuned
2007-10-10 paulson 2007-10-10 more metis proofs
2007-10-09 paulson 2007-10-09 context-based treatment of generalization; also handling TFrees in axiom clauses
2007-10-05 paulson 2007-10-05 metis method: used theorems
2007-09-06 paulson 2007-09-06 new proofs found
2007-07-16 paulson 2007-07-16 tidied using sledgehammer
2007-06-29 paulson 2007-06-29 bug fixes to proof reconstruction
2007-06-23 nipkow 2007-06-23 tuned and renamed group_eq_simps and ring_eq_simps
2007-06-21 wenzelm 2007-06-21 tuned proofs -- avoid implicit prems;
2007-06-21 paulson 2007-06-21 integration of Metis prover