src/HOL/Metis_Examples/Sets.thy
Thu, 15 Feb 2018 12:11:00 +0100 wenzelm more symbols;
Thu, 26 May 2016 17:51:22 +0200 wenzelm isabelle update_cartouches -c -t;
Tue, 01 Sep 2015 22:32:58 +0200 wenzelm eliminated \<Colon>;
Sun, 02 Nov 2014 18:21:45 +0100 wenzelm modernized header uniformly as section;
Thu, 12 Jun 2014 17:10:12 +0200 blanchet renamed Sledgehammer options
Thu, 30 Jan 2014 14:37:53 +0100 blanchet renamed Sledgehammer options for symmetry between positive and negative versions
Tue, 13 Aug 2013 16:25:47 +0200 wenzelm standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
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
Thu, 31 May 2012 15:47:06 +0200 huffman definition less_int_def has changed, use 'less_le' instead
Mon, 02 Jan 2012 15:15:46 +0100 blanchet ported "Sets" example to "set" type constructor
Sat, 24 Dec 2011 15:53:11 +0100 haftmann commented out examples which choke on strict set/pred distinction
Mon, 06 Jun 2011 20:36:35 +0200 blanchet tuned Metis examples
less more (0) tip