src/HOL/ex/Refute_Examples.thy
Wed, 31 Oct 2012 11:23:21 +0100 blanchet fixes related to Refute's move
Fri, 12 Oct 2012 18:58:20 +0200 wenzelm discontinued obsolete typedef (open) syntax;
Tue, 03 Jan 2012 18:33:18 +0100 blanchet reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
Sat, 24 Dec 2011 15:53:11 +0100 haftmann commented out examples which choke on strict set/pred distinction
Wed, 30 Nov 2011 16:27:10 +0100 wenzelm prefer typedef without extra definition and alternative name;
Tue, 08 Jun 2010 16:37:22 +0200 haftmann tuned quotes, antiquotations and whitespace
Fri, 23 Apr 2010 23:35:43 +0200 wenzelm mark schematic statements explicitly;
Tue, 13 Apr 2010 15:30:15 +0200 blanchet adapt Refute example to reflect latest soundness fix to Refute
Mon, 01 Mar 2010 13:40:23 +0100 haftmann replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
Tue, 23 Feb 2010 10:11:12 +0100 haftmann dropped axclass
Mon, 14 Dec 2009 12:14:12 +0100 blanchet added "no_assms" option to Refute, and include structured proof assumptions by default;
Sat, 17 Oct 2009 16:34:39 +0200 wenzelm tuned;
Tue, 07 Oct 2008 16:07:50 +0200 haftmann arbitrary is undefined
Mon, 15 Oct 2007 01:57:50 +0200 webertj interpreter for List.append added again
Mon, 15 Oct 2007 01:36:22 +0200 webertj quick_and_dirty (again) not touched anymore
less more (0) -15 tip