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) | file | diff | annotate |
Tue, 06 Nov 2012 15:15:33 +0100 | blanchet | renamed Sledgehammer option | file | diff | annotate |
Thu, 18 Oct 2012 15:05:17 +0200 | blanchet | renamed Isar-proof related options + changed semantics of Isar shrinking | file | diff | annotate |
Thu, 31 May 2012 15:47:06 +0200 | huffman | definition less_int_def has changed, use 'less_le' instead | file | diff | annotate |
Mon, 02 Jan 2012 15:15:46 +0100 | blanchet | ported "Sets" example to "set" type constructor | file | diff | annotate |
Sat, 24 Dec 2011 15:53:11 +0100 | haftmann | commented out examples which choke on strict set/pred distinction | file | diff | annotate |
Mon, 06 Jun 2011 20:36:35 +0200 | blanchet | tuned Metis examples | file | diff | annotate | base |