| 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
|
| Wed, 10 Aug 2016 09:33:54 +0200 |
nipkow |
"split add" -> "split"
|
file |
diff |
annotate
|
| Mon, 28 Dec 2015 23:13:33 +0100 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Thu, 10 Dec 2015 21:39:33 +0100 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
| Sat, 18 Jul 2015 20:54:56 +0200 |
wenzelm |
prefer tactics with explicit context;
|
file |
diff |
annotate
|
| Tue, 10 Feb 2015 14:48:26 +0100 |
wenzelm |
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
|
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
|
| Thu, 13 Mar 2014 07:07:07 +0100 |
nipkow |
enhanced simplifier solver for preconditions of rewrite rule, can now deal with conjunctions
|
file |
diff |
annotate
|
| Wed, 12 Feb 2014 08:35:57 +0100 |
blanchet |
adapted theories to 'xxx_case' to 'case_xxx'
|
file |
diff |
annotate
|
| Thu, 18 Apr 2013 17:07:01 +0200 |
wenzelm |
simplifier uses proper Proof.context instead of historic type simpset;
|
file |
diff |
annotate
|
| Fri, 18 Feb 2011 15:46:13 +0100 |
wenzelm |
modernized specifications;
|
file |
diff |
annotate
|
| Fri, 10 Sep 2010 15:36:49 +0200 |
wenzelm |
removed spurious addition from 9e58f0499f57;
|
file |
diff |
annotate
|
| Thu, 09 Sep 2010 16:47:03 +0100 |
paulson |
Tidied up proofs using sledgehammer, also deleting unnecessary semicolons
|
file |
diff |
annotate
|
| Wed, 08 Sep 2010 19:21:46 +0200 |
haftmann |
modernized primrec
|
file |
diff |
annotate
|
| Thu, 22 Jul 2010 18:08:39 +0200 |
wenzelm |
updated some headers;
|
file |
diff |
annotate
|
| Mon, 21 Sep 2009 15:33:39 +0200 |
haftmann |
tuned header
|
file |
diff |
annotate
|
| Thu, 23 Jul 2009 18:44:09 +0200 |
wenzelm |
renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;
|
file |
diff |
annotate
|
| Mon, 16 Mar 2009 18:24:30 +0100 |
wenzelm |
simplified method setup;
|
file |
diff |
annotate
|
| Fri, 13 Mar 2009 19:58:26 +0100 |
wenzelm |
unified type Proof.method and pervasive METHOD combinators;
|
file |
diff |
annotate
|
| Wed, 01 Aug 2007 20:25:16 +0200 |
wenzelm |
tuned ML bindings (for multithreading);
|
file |
diff |
annotate
|
| Sat, 21 Jul 2007 23:25:00 +0200 |
wenzelm |
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
|
file |
diff |
annotate
|
| Mon, 11 Jun 2007 11:06:04 +0200 |
chaieb |
tuned Proof
|
file |
diff |
annotate
|
| Fri, 01 Dec 2006 17:22:28 +0100 |
haftmann |
stripped some legacy bindings
|
file |
diff |
annotate
|
| Wed, 29 Nov 2006 15:44:51 +0100 |
wenzelm |
simplified method setup;
|
file |
diff |
annotate
|
| Fri, 17 Nov 2006 02:20:03 +0100 |
wenzelm |
more robust syntax for definition/abbreviation/notation;
|
file |
diff |
annotate
|
| Thu, 28 Sep 2006 23:42:35 +0200 |
wenzelm |
replaced syntax/translations by abbreviation;
|
file |
diff |
annotate
|
| Sat, 08 Jul 2006 12:54:36 +0200 |
wenzelm |
tactic/method simpset: maintain proper context;
|
file |
diff |
annotate
|