| Fri, 12 Oct 2012 18:58:20 +0200 |
wenzelm |
discontinued obsolete typedef (open) syntax;
|
file |
diff |
annotate
|
| Tue, 03 Jan 2012 18:33:18 +0100 |
blanchet |
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
|
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
|
| Wed, 30 Nov 2011 16:27:10 +0100 |
wenzelm |
prefer typedef without extra definition and alternative name;
|
file |
diff |
annotate
|
| Tue, 08 Jun 2010 16:37:22 +0200 |
haftmann |
tuned quotes, antiquotations and whitespace
|
file |
diff |
annotate
|
| Fri, 23 Apr 2010 23:35:43 +0200 |
wenzelm |
mark schematic statements explicitly;
|
file |
diff |
annotate
|
| Tue, 13 Apr 2010 15:30:15 +0200 |
blanchet |
adapt Refute example to reflect latest soundness fix to Refute
|
file |
diff |
annotate
|
| Mon, 01 Mar 2010 13:40:23 +0100 |
haftmann |
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
|
file |
diff |
annotate
|
| Tue, 23 Feb 2010 10:11:12 +0100 |
haftmann |
dropped axclass
|
file |
diff |
annotate
|
| Mon, 14 Dec 2009 12:14:12 +0100 |
blanchet |
added "no_assms" option to Refute, and include structured proof assumptions by default;
|
file |
diff |
annotate
|
| Sat, 17 Oct 2009 16:34:39 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 07 Oct 2008 16:07:50 +0200 |
haftmann |
arbitrary is undefined
|
file |
diff |
annotate
|
| Mon, 15 Oct 2007 01:57:50 +0200 |
webertj |
interpreter for List.append added again
|
file |
diff |
annotate
|
| Mon, 15 Oct 2007 01:36:22 +0200 |
webertj |
quick_and_dirty (again) not touched anymore
|
file |
diff |
annotate
|
| Fri, 12 Oct 2007 22:00:47 +0200 |
webertj |
significant code overhaul, bugfix for inductive data types
|
file |
diff |
annotate
|
| Tue, 28 Aug 2007 11:25:32 +0200 |
wenzelm |
do not touch quick_and_dirty;
|
file |
diff |
annotate
|
| Wed, 11 Jul 2007 11:54:21 +0200 |
berghofe |
Adapted to new inductive definition package.
|
file |
diff |
annotate
|
| Sun, 03 Jun 2007 23:16:47 +0200 |
wenzelm |
tuned document;
|
file |
diff |
annotate
|
| Wed, 07 Feb 2007 18:12:02 +0100 |
berghofe |
Adapted to changes in Finite_Set theory.
|
file |
diff |
annotate
|
| Fri, 19 Jan 2007 22:04:22 +0100 |
webertj |
interpreter for Finite_Set.finite added
|
file |
diff |
annotate
|
| Thu, 04 Jan 2007 00:12:30 +0100 |
webertj |
constants are unfolded, universal quantifiers are stripped, some minor changes
|
file |
diff |
annotate
|
| Mon, 27 Nov 2006 17:35:50 +0100 |
webertj |
outermost universal quantifiers are stripped
|
file |
diff |
annotate
|
| Thu, 23 Nov 2006 20:34:21 +0100 |
wenzelm |
prefer antiquotations over LaTeX macros;
|
file |
diff |
annotate
|
| Thu, 26 Jan 2006 20:17:54 +0100 |
webertj |
smaller example to prevent timeout
|
file |
diff |
annotate
|
| Tue, 24 Jan 2006 15:16:06 +0100 |
webertj |
works with DPLL solver now
|
file |
diff |
annotate
|
| Tue, 26 Jul 2005 12:13:35 +0200 |
webertj |
minor parameter changes
|
file |
diff |
annotate
|
| Mon, 23 May 2005 17:17:06 +0200 |
webertj |
interpreters for lfp/gfp added
|
file |
diff |
annotate
|
| Mon, 18 Apr 2005 17:20:49 +0200 |
webertj |
support for recursion over mutually recursive IDTs
|
file |
diff |
annotate
|
| Wed, 23 Feb 2005 14:04:53 +0100 |
webertj |
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
|
file |
diff |
annotate
|
| Thu, 18 Nov 2004 18:46:09 +0100 |
webertj |
imports (new syntax for theory headers)
|
file |
diff |
annotate
|