| Mon, 31 Jan 2022 16:09:23 +0100 |
blanchet |
compile Metis_Examples
|
file |
diff |
annotate
|
| Tue, 22 Jan 2019 12:00:16 +0000 |
paulson |
renamings and new material
|
file |
diff |
annotate
|
| Tue, 15 May 2018 11:33:43 +0200 |
immler |
move FuncSet back to HOL-Library (amending 493b818e8e10)
|
file |
diff |
annotate
|
| Wed, 02 May 2018 13:49:38 +0200 |
immler |
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
|
file |
diff |
annotate
|
| Wed, 10 Jan 2018 15:25:09 +0100 |
nipkow |
ran isabelle update_op on all sources
|
file |
diff |
annotate
|
| Fri, 18 Aug 2017 20:47:47 +0200 |
wenzelm |
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
|
file |
diff |
annotate
|
| Thu, 26 May 2016 17:51:22 +0200 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
| Sat, 10 Oct 2015 19:22:05 +0200 |
wenzelm |
prefer symbols;
|
file |
diff |
annotate
|
| Sun, 02 Nov 2014 18:21:45 +0100 |
wenzelm |
modernized header uniformly as section;
|
file |
diff |
annotate
|
| Thu, 06 Mar 2014 13:36:48 +0100 |
blanchet |
renamed 'map_pair' to 'map_prod'
|
file |
diff |
annotate
|
| Fri, 14 Feb 2014 07:53:45 +0100 |
blanchet |
merged 'List.map' and 'List.list.map'
|
file |
diff |
annotate
|
| Mon, 30 Jan 2012 17:15:59 +0100 |
blanchet |
example tuning
|
file |
diff |
annotate
|
| Mon, 02 Jan 2012 15:08:40 +0100 |
blanchet |
ported a dozen of proofs to the "set" type constructor
|
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
|
| Fri, 18 Nov 2011 11:47:12 +0100 |
blanchet |
more "metis" calls in example
|
file |
diff |
annotate
|
| Fri, 18 Nov 2011 11:47:12 +0100 |
blanchet |
example cleanup
|
file |
diff |
annotate
|
| Fri, 18 Nov 2011 11:47:12 +0100 |
blanchet |
example cleanup
|
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
|
| Thu, 12 May 2011 15:29:19 +0200 |
blanchet |
remove problematic Isar proof
|
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, 29 Dec 2010 17:34:41 +0100 |
wenzelm |
explicit file specifications -- avoid secondary load path;
|
file |
diff |
annotate
|
| Wed, 15 Dec 2010 11:26:28 +0100 |
blanchet |
example tuning
|
file |
diff |
annotate
|
| Wed, 01 Sep 2010 00:07:31 +0200 |
blanchet |
rename sledgehammer config attributes
|
file |
diff |
annotate
|
| Fri, 30 Apr 2010 14:00:09 +0200 |
blanchet |
minor improvements
|
file |
diff |
annotate
|
| Thu, 29 Apr 2010 19:02:04 +0200 |
blanchet |
redid some Sledgehammer/Metis proofs
|
file |
diff |
annotate
|
| Tue, 20 Oct 2009 19:52:04 +0200 |
wenzelm |
modernized session Metis_Examples;
|
file |
diff |
annotate
| base
|