| Tue, 07 Nov 2017 14:52:27 +0100 |
nipkow |
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
|
file |
diff |
annotate
|
| Mon, 17 Oct 2016 11:46:22 +0200 |
nipkow |
setsum -> sum
|
file |
diff |
annotate
|
| Thu, 15 Sep 2016 11:48:20 +0200 |
nipkow |
renamed listsum -> sum_list, listprod ~> prod_list
|
file |
diff |
annotate
|
| Sat, 19 Dec 2015 11:05:04 +0100 |
haftmann |
abandoned attempt to unify sublocale and interpretation into global theories
|
file |
diff |
annotate
|
| Sat, 14 Nov 2015 08:45:52 +0100 |
haftmann |
prefer "rewrites" and "defines" to note rewrite morphisms
|
file |
diff |
annotate
|
| Tue, 15 Sep 2015 17:09:13 +0200 |
nipkow |
goali -> i
|
file |
diff |
annotate
|
| Wed, 19 Feb 2014 22:05:15 +0100 |
haftmann |
more convenient syntax for permanent interpretation
|
file |
diff |
annotate
|
| Wed, 19 Feb 2014 22:05:05 +0100 |
haftmann |
aggiornamento for "interpretation with definitions": operate uniformly on theory and locale level under the brand of "permanent interpretation"
|
file |
diff |
annotate
|
| Fri, 07 Feb 2014 14:18:31 +0100 |
nipkow |
fight spurious nitpick timeouts
|
file |
diff |
annotate
|
| Tue, 13 Aug 2013 16:25:47 +0200 |
wenzelm |
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
|
file |
diff |
annotate
|
| Thu, 25 Jul 2013 08:57:16 +0200 |
haftmann |
factored syntactic type classes for bot and top (by Alessandro Coglio)
|
file |
diff |
annotate
|
| Wed, 03 Jul 2013 16:07:00 +0200 |
nipkow |
tuned names
|
file |
diff |
annotate
|
| Thu, 16 May 2013 02:13:23 +0200 |
nipkow |
finally: acom with pointwise access and update of annotations
|
file |
diff |
annotate
|
| Tue, 14 May 2013 06:54:31 +0200 |
nipkow |
tuned names
|
file |
diff |
annotate
|
| Mon, 13 May 2013 06:50:37 +0200 |
nipkow |
tuned names
|
file |
diff |
annotate
|
| Thu, 09 May 2013 03:58:28 +0200 |
nipkow |
standard ivl notation [l,h]
|
file |
diff |
annotate
|
| Wed, 08 May 2013 06:14:11 +0200 |
nipkow |
tuned
|
file |
diff |
annotate
|
| Tue, 07 May 2013 10:34:55 +0200 |
nipkow |
tuned name: filter -> constrain (longer but more intuitive)
|
file |
diff |
annotate
|
| Tue, 30 Apr 2013 03:18:07 +0200 |
nipkow |
canonical names of classes
|
file |
diff |
annotate
|
| Fri, 26 Apr 2013 13:23:21 +0200 |
nipkow |
simplified def
|
file |
diff |
annotate
|
| Fri, 26 Apr 2013 13:12:14 +0200 |
nipkow |
more standard argument order
|
file |
diff |
annotate
|
| Fri, 26 Apr 2013 09:53:11 +0200 |
nipkow |
simplified def
|
file |
diff |
annotate
|
| Fri, 26 Apr 2013 09:41:45 +0200 |
nipkow |
more standard order of arguments
|
file |
diff |
annotate
|
| Sat, 20 Apr 2013 20:57:49 +0200 |
nipkow |
proved termination for fun-based AI
|
file |
diff |
annotate
|
| Wed, 17 Apr 2013 21:11:01 +0200 |
nipkow |
complete revision: finally got rid of annoying L-predicate
|
file |
diff |
annotate
|
| Mon, 11 Mar 2013 12:27:31 +0100 |
nipkow |
more factorisation of Step & Co
|
file |
diff |
annotate
|
| Sun, 10 Mar 2013 10:10:01 +0100 |
nipkow |
termination proof for narrowing: fewer assumptions
|
file |
diff |
annotate
|
| Fri, 08 Mar 2013 11:28:04 +0100 |
nipkow |
simplified basic termination proof
|
file |
diff |
annotate
|
| Wed, 06 Mar 2013 16:10:56 +0100 |
nipkow |
major redesign: order instead of preorder, new definition of intervals as quotients
|
file |
diff |
annotate
|
| Fri, 22 Feb 2013 20:12:53 +0100 |
nipkow |
more abstract intervals
|
file |
diff |
annotate
|