Fri, 23 Apr 2010 23:35:43 +0200 |
wenzelm |
mark schematic statements explicitly;
|
file |
diff |
annotate
|
Mon, 01 Mar 2010 17:45:02 +0100 |
wenzelm |
repaired 'definition' (cf. d8d7d1b785af);
|
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
|
Wed, 24 Feb 2010 11:55:52 +0100 |
blanchet |
compile
|
file |
diff |
annotate
|
Wed, 24 Feb 2010 11:35:10 +0100 |
blanchet |
compile
|
file |
diff |
annotate
|
Wed, 24 Feb 2010 09:59:54 +0100 |
blanchet |
got rid of "axclass", apparently
|
file |
diff |
annotate
|
Mon, 22 Feb 2010 19:31:00 +0100 |
blanchet |
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
|
file |
diff |
annotate
|
Wed, 10 Feb 2010 11:47:33 +0100 |
blanchet |
make Nitpick test a bit weaker;
|
file |
diff |
annotate
|
Tue, 09 Feb 2010 16:07:51 +0100 |
blanchet |
optimization to quantifiers in Nitpick's handling of simp rules + renamed some SAT solvers
|
file |
diff |
annotate
|
Fri, 05 Feb 2010 14:27:21 +0100 |
blanchet |
added hotel key card example for Nitpick, and renumber atoms in Nitpick's output for increased readability
|
file |
diff |
annotate
|
Mon, 14 Dec 2009 10:59:46 +0100 |
blanchet |
make Nitpick tests more robust by specifying SAT solver, singlethreading (in Kodkod, not in Isabelle), and higher time limits
|
file |
diff |
annotate
|
Tue, 17 Nov 2009 13:51:16 +0100 |
blanchet |
use SAT solver that's available everywhere for this example
|
file |
diff |
annotate
|
Fri, 23 Oct 2009 18:59:24 +0200 |
blanchet |
continuation of Nitpick's integration into Isabelle;
|
file |
diff |
annotate
|