1.1 --- a/NEWS Tue May 16 21:33:21 2006 +0200
1.2 +++ b/NEWS Tue May 16 21:33:23 2006 +0200
1.3 @@ -148,21 +148,19 @@
1.4 explicit (is "_ ==> ?foo") in the rare cases where this still happens
1.5 to occur.
1.6
1.7 -* Isar/locales: new derived specification elements 'definition',
1.8 -'abbreviation', 'axiomatization', which support type-inference, admit
1.9 +* Isar/locales: new derived specification elements 'axiomatization',
1.10 +'definition', 'abbreviation', which support type-inference, admit
1.11 object-level specifications (equality, equivalence). See also the
1.12 isar-ref manual. Examples:
1.13
1.14 + axiomatization
1.15 + eq (infix "===" 50)
1.16 + where eq_refl: "x === x" and eq_subst: "x === y ==> P x ==> P y"
1.17 +
1.18 definition
1.19 "f x y = x + y + 1"
1.20 "g x = f x x"
1.21
1.22 - thm f_def g_def
1.23 -
1.24 - axiomatization
1.25 - eq (infix "===" 50)
1.26 - where eq_refl: "x === x" and eq_subst: "x === y ==> P x ==> P y"
1.27 -
1.28 abbreviation
1.29 neq (infix "=!=" 50)
1.30 "x =!= y == ~ (x === y)"
1.31 @@ -180,6 +178,11 @@
1.32 'abbreviation' may be used as a type-safe replacement for 'syntax' +
1.33 'translations' in common applications.
1.34
1.35 +* Isar/locales: 'const_syntax' provides a robust interface to the
1.36 +'syntax' primitive that also works in a locale context. Type
1.37 +declaration and internal syntactic representation of given constants
1.38 +retrieved from the context.
1.39 +
1.40 * Provers/induct: improved internal context management to support
1.41 local fixes and defines on-the-fly. Thus explicit meta-level
1.42 connectives !! and ==> are rarely required anymore in inductive goals