| Fri, 20 Sep 2024 19:51:08 +0200 |
wenzelm |
standardize mixfix annotations via "isabelle update -a -u mixfix_cartouches" --- to simplify systematic editing;
|
file |
diff |
annotate
|
| Thu, 08 Jul 2021 08:42:36 +0200 |
desharna |
added opaque_combs and renamed hide_lams to opaque_lifting
|
file |
diff |
annotate
|
| Thu, 11 Mar 2021 07:05:38 +0000 |
haftmann |
avoid name clash
|
file |
diff |
annotate
|
| Sat, 05 Jan 2019 17:24:33 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| Wed, 26 Dec 2018 16:25:20 +0100 |
wenzelm |
isabelle update_cartouches -t;
|
file |
diff |
annotate
|
| Tue, 21 Aug 2018 17:29:46 +0200 |
nipkow |
improved sectioning
|
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
|
| Fri, 12 Jan 2018 14:08:53 +0100 |
wenzelm |
isabelle update_cartouches -c;
|
file |
diff |
annotate
|
| Wed, 10 Jan 2018 15:25:09 +0100 |
nipkow |
ran isabelle update_op on all sources
|
file |
diff |
annotate
|
| 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
|