| Wed, 19 Oct 2022 15:34:41 +0100 |
paulson |
Tidying of old and ugly proofs
|
file |
diff |
annotate
|
| Wed, 19 Oct 2022 13:41:42 +0100 |
paulson |
deleted unused material
|
file |
diff |
annotate
|
| Tue, 22 Jan 2019 12:00:16 +0000 |
paulson |
renamings and new material
|
file |
diff |
annotate
|
| Sat, 05 Jan 2019 17:24:33 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| Thu, 15 Feb 2018 12:11:00 +0100 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Tue, 16 Jan 2018 09:30:00 +0100 |
wenzelm |
standardized towards new-style formal comments: isabelle update_comments;
|
file |
diff |
annotate
|
| Thu, 26 May 2016 17:51:22 +0200 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
| Tue, 23 Feb 2016 16:25:08 +0100 |
nipkow |
more canonical names
|
file |
diff |
annotate
|
| Wed, 30 Dec 2015 18:17:28 +0100 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Tue, 01 Sep 2015 22:32:58 +0200 |
wenzelm |
eliminated \<Colon>;
|
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
|
| Tue, 09 Sep 2014 20:51:36 +0200 |
blanchet |
use 'datatype_new' (soon to be renamed 'datatype') in Isabelle's libraries
|
file |
diff |
annotate
|
| Tue, 13 Aug 2013 16:25:47 +0200 |
wenzelm |
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
|
file |
diff |
annotate
|
| 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)
|
file |
diff |
annotate
|
| Mon, 02 Jan 2012 14:45:13 +0100 |
blanchet |
reintroduced "metis" call taken out after reintroducing "set" as a constructor, and added two "metis" calls that used to be too slow
|
file |
diff |
annotate
|
| Sat, 24 Dec 2011 15:53:10 +0100 |
haftmann |
adjusted to set/pred distinction by means of type constructor `set`
|
file |
diff |
annotate
|
| Sun, 20 Nov 2011 21:05:23 +0100 |
wenzelm |
eliminated obsolete "standard";
|
file |
diff |
annotate
|
| Tue, 15 Nov 2011 12:51:14 +0100 |
huffman |
remove one more old-style semicolon
|
file |
diff |
annotate
|
| Tue, 15 Nov 2011 12:39:49 +0100 |
huffman |
remove old-style semicolons
|
file |
diff |
annotate
|
| Mon, 06 Jun 2011 20:36:35 +0200 |
blanchet |
tuned Metis examples
|
file |
diff |
annotate
|
| Sat, 23 Apr 2011 13:00:19 +0200 |
wenzelm |
modernized specifications;
|
file |
diff |
annotate
|
| Thu, 24 Mar 2011 17:49:27 +0100 |
blanchet |
Metis examples use the new Skolemizer to test it
|
file |
diff |
annotate
|
| Wed, 15 Dec 2010 11:26:28 +0100 |
blanchet |
example tuning
|
file |
diff |
annotate
|
| Wed, 15 Dec 2010 11:26:28 +0100 |
blanchet |
added example to exercise higher-order reasoning with Sledgehammer and Metis
|
file |
diff |
annotate
|
| Thu, 09 Sep 2010 12:28:00 +0200 |
blanchet |
"resurrected" a Metis proof
|
file |
diff |
annotate
|
| Fri, 14 May 2010 11:24:49 +0200 |
blanchet |
improved Sledgehammer proofs
|
file |
diff |
annotate
|
| Fri, 30 Apr 2010 18:29:04 +0200 |
wenzelm |
eliminated spurious sledgehammer invocation;
|
file |
diff |
annotate
|
| Wed, 28 Apr 2010 22:36:39 +0200 |
blanchet |
redo some of the metis proofs
|
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
|