summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Tue, 16 May 2006 21:33:23 +0200 | |

changeset 19665 | 8885951e9c2d |

parent 19664 | e1dc01a48a52 |

child 19666 | eee5e8dbda59 |

* Isar/locale: 'const_syntax';

--- a/NEWS Tue May 16 21:33:21 2006 +0200 +++ b/NEWS Tue May 16 21:33:23 2006 +0200 @@ -148,21 +148,19 @@ explicit (is "_ ==> ?foo") in the rare cases where this still happens to occur. -* Isar/locales: new derived specification elements 'definition', -'abbreviation', 'axiomatization', which support type-inference, admit +* Isar/locales: new derived specification elements 'axiomatization', +'definition', 'abbreviation', which support type-inference, admit object-level specifications (equality, equivalence). See also the isar-ref manual. Examples: + axiomatization + eq (infix "===" 50) + where eq_refl: "x === x" and eq_subst: "x === y ==> P x ==> P y" + definition "f x y = x + y + 1" "g x = f x x" - thm f_def g_def - - axiomatization - eq (infix "===" 50) - where eq_refl: "x === x" and eq_subst: "x === y ==> P x ==> P y" - abbreviation neq (infix "=!=" 50) "x =!= y == ~ (x === y)" @@ -180,6 +178,11 @@ 'abbreviation' may be used as a type-safe replacement for 'syntax' + 'translations' in common applications. +* Isar/locales: 'const_syntax' provides a robust interface to the +'syntax' primitive that also works in a locale context. Type +declaration and internal syntactic representation of given constants +retrieved from the context. + * Provers/induct: improved internal context management to support local fixes and defines on-the-fly. Thus explicit meta-level connectives !! and ==> are rarely required anymore in inductive goals