2008-05-07 berghofe 2008-05-07 Adapted to encoding of sets as predicates
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;
2007-12-19 paulson 2007-12-19 Replaced refs by config params; finer critical section in mets method
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-27 paulson 2007-09-27 removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering theorems of Nat.thy are hidden by the Ordering.thy versions
2007-06-29 paulson 2007-06-29 bug fixes to proof reconstruction
2007-06-21 paulson 2007-06-21 integration of Metis prover