| #
5589896c |
|
12-Jan-2018 |
wenzelm <none@none> |
isabelle update_cartouches -c;
|
| #
c32926df |
|
17-Dec-2016 |
haftmann <none@none> |
reoriented congruence rules in non-explosive direction
--HG--
extra : rebase_source : 7b0d0d20a7c78db1ac5f12fb0d4ab0d915d0f2a3
|
| #
7b0aa853 |
|
19-Dec-2015 |
haftmann <none@none> |
abandoned attempt to unify sublocale and interpretation into global theories
|
| #
b2dfeb3f |
|
14-Nov-2015 |
haftmann <none@none> |
prefer "rewrites" and "defines" to note rewrite morphisms
--HG--
extra : rebase_source : db946849cc605955aa705d31965275c62fa42379
|
| #
db4d66be |
|
15-Sep-2015 |
nipkow <none@none> |
goali -> i
|
| #
5fc26177 |
|
11-Sep-2014 |
blanchet <none@none> |
updated news
|
| #
d2ddb3a1 |
|
09-Sep-2014 |
blanchet <none@none> |
use 'datatype_new' (soon to be renamed 'datatype') in Isabelle's libraries
|
| #
a8dfe60c |
|
09-May-2014 |
haftmann <none@none> |
hardcoded nbe and sml into value command
|
| #
c3bd9e8d |
|
19-Feb-2014 |
haftmann <none@none> |
more convenient syntax for permanent interpretation
--HG--
extra : rebase_source : 2a04f8fb415c90b0857d9553e69987e69e438c11
|
| #
d019087e |
|
19-Feb-2014 |
haftmann <none@none> |
aggiornamento for "interpretation with definitions": operate uniformly on theory and locale level under the brand of "permanent interpretation"
--HG--
extra : rebase_source : 0e0256451de0363834f9d89306c7198ad6a4e2b2
|
| #
f5c99619 |
|
05-Jul-2013 |
nipkow <none@none> |
tund proofs
|
| #
747b2ee1 |
|
03-Jul-2013 |
nipkow <none@none> |
tuned names
|
| #
83572917 |
|
17-May-2013 |
nipkow <none@none> |
replaced `;' by `;;' to disambiguate syntax; unexpected slight increase in build time
|
| #
619d5137 |
|
29-Apr-2013 |
nipkow <none@none> |
canonical names of classes
|
| #
772233d8 |
|
17-Apr-2013 |
nipkow <none@none> |
complete revision: finally got rid of annoying L-predicate
|
| #
b8968364 |
|
05-Apr-2013 |
nipkow <none@none> |
tuned document
|
| #
00bec273 |
|
05-Apr-2013 |
nipkow <none@none> |
tuned
|
| #
a7bab1ad |
|
10-Mar-2013 |
nipkow <none@none> |
factored out Step
|
| #
458d320c |
|
08-Mar-2013 |
nipkow <none@none> |
simplified basic termination proof
|
| #
f06c7f68 |
|
06-Mar-2013 |
nipkow <none@none> |
major redesign: order instead of preorder, new definition of intervals as quotients
|
| #
e9783ae7 |
|
12-Feb-2013 |
nipkow <none@none> |
tuned top
|
| #
eb80be15 |
|
25-Jan-2013 |
nipkow <none@none> |
tuned
|
| #
7eae9c54 |
|
17-Sep-2012 |
nipkow <none@none> |
tuned
|
| #
ffb47d43 |
|
16-Sep-2012 |
nipkow <none@none> |
tuned
|
| #
3f59dca8 |
|
16-Sep-2012 |
nipkow <none@none> |
converted wt into a set, tuned names
|
| #
8d45020a |
|
13-Sep-2012 |
nipkow <none@none> |
tuned
|
| #
5e83833a |
|
06-Sep-2012 |
nipkow <none@none> |
adjusted examples
|
| #
23bc83b2 |
|
19-Apr-2012 |
nipkow <none@none> |
added revised version of Abs_Int
|