src/HOL/Metis_Examples/Trans_Closure.thy
Thu, 14 Feb 2013 22:49:22 +0100 smolkas renamed sledgehammer_shrink to sledgehammer_compress
Thu, 03 Jan 2013 17:28:55 +0100 blanchet use new skolemizer for reconstructing skolemization steps in Isar proofs (because the old skolemizer messes up the order of the Skolem arguments)
Tue, 06 Nov 2012 15:15:33 +0100 blanchet renamed Sledgehammer option
Thu, 18 Oct 2012 15:05:17 +0200 blanchet renamed Isar-proof related options + changed semantics of Isar shrinking
Sat, 24 Dec 2011 15:53:10 +0100 haftmann adjusted to set/pred distinction by means of type constructor `set`
Mon, 06 Jun 2011 20:36:35 +0200 blanchet tuned Metis examples
less more (0) tip