Tue, 07 Nov 2017 14:52:27 +0100 |
nipkow |
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
|
file |
diff |
annotate
|
Fri, 22 Jul 2016 11:00:43 +0200 |
wenzelm |
tuned proofs -- avoid unstructured calculation;
|
file |
diff |
annotate
|
Tue, 23 Feb 2016 16:25:08 +0100 |
nipkow |
more canonical names
|
file |
diff |
annotate
|
Thu, 10 Sep 2015 11:03:29 +0200 |
nipkow |
tuned
|
file |
diff |
annotate
|
Thu, 20 Mar 2014 09:47:43 +0100 |
kleing |
pointer to the other proof direction
|
file |
diff |
annotate
|
Thu, 26 Sep 2013 11:41:01 +0200 |
nipkow |
tuned
|
file |
diff |
annotate
|
Wed, 25 Sep 2013 15:49:09 +0200 |
nipkow |
tuned
|
file |
diff |
annotate
|
Sun, 01 Sep 2013 16:38:04 +1000 |
kleing |
remove redundant (simp del: ..)
|
file |
diff |
annotate
|
Thu, 08 Aug 2013 18:13:12 +0200 |
kleing |
avoid re-inventing transitive closure
|
file |
diff |
annotate
|
Thu, 20 Jun 2013 17:26:16 +0200 |
nipkow |
tuned theory name
|
file |
diff |
annotate
| base
|