src/HOL/MetisExamples/BigO.thy
2008-05-07 berghofe 2008-05-07 Replaced + and * on sets by \<oplus> and \<otimes>, to avoid clash with definitions of + and * on functions.
2008-04-14 ballarin 2008-04-14 Changed naming scheme for theorems generated by interpretations.
2008-03-29 wenzelm 2008-03-29 replaced 'ML' by diagnostic 'ML_command';
2008-03-19 paulson 2008-03-19 Attributes sledgehammer_full, sledgehammer_modulus, sledgehammer_sorts Sledgehammer no longer produces structured proofs by default.
2008-03-17 wenzelm 2008-03-17 avoid rebinding of existing facts;
2008-02-27 chaieb 2008-02-27 Fixed dependency on Dense_Linear_Order
2008-02-06 haftmann 2008-02-06 locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
2007-12-19 paulson 2007-12-19 Replaced refs by config params; finer critical section in mets method
2007-12-10 haftmann 2007-12-10 explicit import of theory Main
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