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
|