| Tue, 06 Oct 2015 17:47:28 +0200 |
wenzelm |
isabelle update_cartouches;
|
file |
diff |
annotate
|
| Tue, 06 Oct 2015 15:14:28 +0200 |
wenzelm |
fewer aliases for toplevel theorem statements;
|
file |
diff |
annotate
|
| Thu, 09 Apr 2015 18:00:59 +0200 |
blanchet |
removed a refute example that caused trouble with testing
|
file |
diff |
annotate
|
| Sun, 02 Nov 2014 18:21:45 +0100 |
wenzelm |
modernized header uniformly as section;
|
file |
diff |
annotate
|
| Thu, 11 Sep 2014 19:32:36 +0200 |
blanchet |
updated news
|
file |
diff |
annotate
|
| Thu, 11 Sep 2014 18:54:36 +0200 |
blanchet |
renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
|
file |
diff |
annotate
|
| Thu, 11 Sep 2014 18:54:36 +0200 |
blanchet |
took out some datatype tests for Refute -- these yield timeouts on some Isatests after transition to new datatypes, for some reason (and Refute is obsolete anyway)
|
file |
diff |
annotate
|
| Mon, 08 Sep 2014 16:14:21 +0200 |
blanchet |
adapted examples to latest changes
|
file |
diff |
annotate
|
| Thu, 04 Sep 2014 11:53:39 +0200 |
blanchet |
tuned Nitpick and Refute examples, which are too slow on some testing machines
|
file |
diff |
annotate
|
| Tue, 02 Sep 2014 23:59:49 +0200 |
blanchet |
removed more slow Refute tests
|
file |
diff |
annotate
|
| Tue, 02 Sep 2014 23:59:46 +0200 |
blanchet |
tuned Refute example
|
file |
diff |
annotate
|
| Mon, 01 Sep 2014 17:34:03 +0200 |
blanchet |
ported Refute to use new datatypes when possible
|
file |
diff |
annotate
|
| Sun, 04 May 2014 18:57:45 +0200 |
blanchet |
renamed 'dpll_p' to 'cdclite', to avoid confusion with the old 'dpll' and to reflect the idea that the new prover implements some ideas from CDCL not in DPLL -- this follows its author's, Sascha B.'s, wish
|
file |
diff |
annotate
|
| Sun, 04 May 2014 16:17:53 +0200 |
boehmes |
removed obsolete internal SAT solvers
|
file |
diff |
annotate
|
| Thu, 01 May 2014 22:56:59 +0200 |
boehmes |
added internal proof-producing SAT solver
|
file |
diff |
annotate
|
| Fri, 21 Mar 2014 20:33:56 +0100 |
wenzelm |
more qualified names;
|
file |
diff |
annotate
|
| Mon, 03 Mar 2014 12:48:20 +0100 |
blanchet |
rationalized internals
|
file |
diff |
annotate
|
| Wed, 12 Feb 2014 08:35:57 +0100 |
blanchet |
adapted theories to 'xxx_case' to 'case_xxx'
|
file |
diff |
annotate
|
| Wed, 12 Feb 2014 08:35:57 +0100 |
blanchet |
renamed 'nat_{case,rec}' to '{case,rec}_nat'
|
file |
diff |
annotate
|
| Wed, 12 Feb 2014 08:35:56 +0100 |
blanchet |
adapted theories to '{case,rec}_{list,option}' names
|
file |
diff |
annotate
|
| Wed, 12 Feb 2014 08:35:56 +0100 |
blanchet |
removed trivial 'rec' examples for nonrecursive types (I could also have added the 'old.' prefix in front of the constant names)
|
file |
diff |
annotate
|
| Wed, 31 Oct 2012 11:23:21 +0100 |
blanchet |
fixes related to Refute's move
|
file |
diff |
annotate
|
| 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
|