| #
ab32308e |
|
21-Jan-2019 |
paulson <lp15@cam.ac.uk> |
renamings and new material
|
| #
ed7a971e |
|
05-Jan-2019 |
wenzelm <none@none> |
isabelle update -u control_cartouches;
|
| #
f5796e6d |
|
14-Feb-2018 |
wenzelm <none@none> |
more symbols;
|
| #
5385dbfa |
|
16-Jan-2018 |
wenzelm <none@none> |
standardized towards new-style formal comments: isabelle update_comments;
|
| #
66281660 |
|
26-May-2016 |
wenzelm <none@none> |
isabelle update_cartouches -c -t;
|
| #
35f7dccd |
|
23-Feb-2016 |
nipkow <none@none> |
more canonical names
|
| #
1dd9fadf |
|
30-Dec-2015 |
wenzelm <none@none> |
more symbols;
|
| #
85ed9565 |
|
01-Sep-2015 |
wenzelm <none@none> |
eliminated \<Colon>;
|
| #
794edf80 |
|
02-Nov-2014 |
wenzelm <none@none> |
modernized header uniformly as section;
|
| #
5fc26177 |
|
11-Sep-2014 |
blanchet <none@none> |
updated news
|
| #
d2ddb3a1 |
|
09-Sep-2014 |
blanchet <none@none> |
use 'datatype_new' (soon to be renamed 'datatype') in Isabelle's libraries
|
| #
06329277 |
|
13-Aug-2013 |
wenzelm <none@none> |
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
|
| #
d8eed40e |
|
03-Jan-2013 |
blanchet <none@none> |
use new skolemizer for reconstructing skolemization steps in Isar proofs (because the old skolemizer messes up the order of the Skolem arguments)
|
| #
f7a160b6 |
|
02-Jan-2012 |
blanchet <none@none> |
reintroduced "metis" call taken out after reintroducing "set" as a constructor, and added two "metis" calls that used to be too slow
|
| #
e9912d13 |
|
24-Dec-2011 |
haftmann <none@none> |
adjusted to set/pred distinction by means of type constructor `set`
|
| #
f4961062 |
|
20-Nov-2011 |
wenzelm <none@none> |
eliminated obsolete "standard";
|
| #
d9ddf3dd |
|
14-Nov-2011 |
huffman <none@none> |
remove one more old-style semicolon
|
| #
4e4fcf45 |
|
14-Nov-2011 |
huffman <none@none> |
remove old-style semicolons
|
| #
0b195586 |
|
06-Jun-2011 |
blanchet <none@none> |
tuned Metis examples
--HG--
rename : src/HOL/Metis_Examples/BigO.thy => src/HOL/Metis_Examples/Big_O.thy
rename : src/HOL/Metis_Examples/BT.thy => src/HOL/Metis_Examples/Binary_Tree.thy
rename : src/HOL/Metis_Examples/Clausify.thy => src/HOL/Metis_Examples/Clausification.thy
rename : src/HOL/Metis_Examples/HO_Reas.thy => src/HOL/Metis_Examples/Proxies.thy
rename : src/HOL/Metis_Examples/set.thy => src/HOL/Metis_Examples/Sets.thy
rename : src/HOL/Metis_Examples/TransClosure.thy => src/HOL/Metis_Examples/Trans_Closure.thy
rename : src/HOL/Metis_Examples/Typings.thy => src/HOL/Metis_Examples/Type_Encodings.thy
|
| #
9b4853bb |
|
23-Apr-2011 |
wenzelm <none@none> |
modernized specifications;
|
| #
6d8a56c3 |
|
24-Mar-2011 |
blanchet <none@none> |
Metis examples use the new Skolemizer to test it
|
| #
86ceb3c3 |
|
15-Dec-2010 |
blanchet <none@none> |
example tuning
|
| #
52250154 |
|
15-Dec-2010 |
blanchet <none@none> |
added example to exercise higher-order reasoning with Sledgehammer and Metis
|
| #
0de46e44 |
|
08-Sep-2010 |
blanchet <none@none> |
"resurrected" a Metis proof
|
| #
09676f59 |
|
14-May-2010 |
blanchet <none@none> |
improved Sledgehammer proofs
|
| #
e452c0bc |
|
30-Apr-2010 |
wenzelm <none@none> |
eliminated spurious sledgehammer invocation;
|
| #
d2790a02 |
|
28-Apr-2010 |
blanchet <none@none> |
redo some of the metis proofs
|
| #
baea5702 |
|
01-Mar-2010 |
haftmann <none@none> |
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
|
| #
94b29512 |
|
11-Feb-2010 |
wenzelm <none@none> |
modernized syntax/translations;
|
| #
f7de0e83 |
|
10-Feb-2010 |
haftmann <none@none> |
minor metis proof tuning
|
| #
3403212c |
|
08-Feb-2010 |
wenzelm <none@none> |
modernized some syntax translations;
|
| #
1ee38138 |
|
20-Oct-2009 |
wenzelm <none@none> |
modernized session Metis_Examples;
--HG--
rename : src/HOL/MetisExamples/Abstraction.thy => src/HOL/Metis_Examples/Abstraction.thy
rename : src/HOL/MetisExamples/BT.thy => src/HOL/Metis_Examples/BT.thy
rename : src/HOL/MetisExamples/BigO.thy => src/HOL/Metis_Examples/BigO.thy
rename : src/HOL/MetisExamples/Message.thy => src/HOL/Metis_Examples/Message.thy
rename : src/HOL/MetisExamples/ROOT.ML => src/HOL/Metis_Examples/ROOT.ML
rename : src/HOL/MetisExamples/Tarski.thy => src/HOL/Metis_Examples/Tarski.thy
rename : src/HOL/MetisExamples/TransClosure.thy => src/HOL/Metis_Examples/TransClosure.thy
rename : src/HOL/MetisExamples/set.thy => src/HOL/Metis_Examples/set.thy
|