# HG changeset patch # User wenzelm # Date 1147808003 -7200 # Node ID 8885951e9c2df70ff2375452919916da53ac9cc7 # Parent e1dc01a48a523994539ca03ee927f610449dd2fc * Isar/locale: 'const_syntax'; diff -r e1dc01a48a52 -r 8885951e9c2d NEWS --- 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