| Wed, 13 Oct 2021 00:07:06 +0200 |
wenzelm |
support HOL-Isar_Examples.Hoare as well (amending 403ce50e6a2a);
|
file |
diff |
annotate
|
| Tue, 12 Oct 2021 20:57:43 +0200 |
nipkow |
separated commands from annotations to be able to abstract about the latter only
|
file |
diff |
annotate
|
| Tue, 28 Sep 2021 17:09:05 +0200 |
wenzelm |
tuned antiquotations;
|
file |
diff |
annotate
|
| Sun, 12 Sep 2021 20:52:39 +0200 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
| Wed, 23 Dec 2020 17:16:05 +0100 |
wenzelm |
clarified modules: avoid multiple uses of the same ML file;
|
file |
diff |
annotate
|
| Fri, 04 Dec 2020 15:07:47 +0100 |
nipkow |
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
|
file |
diff |
annotate
|
| Sat, 05 Jan 2019 17:24:33 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| Tue, 13 Oct 2015 09:21:15 +0200 |
haftmann |
prod_case as canonical name for product type eliminator
|
file |
diff |
annotate
|
| Sun, 06 Sep 2015 22:14:51 +0200 |
haftmann |
prefer "uncurry" as canonical name for case distinction on products in combinatorial view
|
file |
diff |
annotate
|
| Sat, 18 Jul 2015 20:54:56 +0200 |
wenzelm |
prefer tactics with explicit context;
|
file |
diff |
annotate
|
| Fri, 21 Feb 2014 20:47:48 +0100 |
wenzelm |
tuned whitespace;
|
file |
diff |
annotate
|
| Fri, 21 Feb 2014 20:37:13 +0100 |
wenzelm |
proper ML structure with signature;
|
file |
diff |
annotate
|
| Fri, 21 Feb 2014 20:29:33 +0100 |
wenzelm |
reduced ML warnings;
|
file |
diff |
annotate
|
| Wed, 12 Feb 2014 08:35:57 +0100 |
blanchet |
renamed '{prod,sum,bool,unit}_case' to 'case_...'
|
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
|