summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

NEWS

changeset 17385 | 4dcae6e62268 |

parent 17371 | 923ef4a8c672 |

child 17389 | b4743198b939 |

--- a/NEWS Wed Sep 14 22:04:35 2005 +0200 +++ b/NEWS Wed Sep 14 22:04:36 2005 +0200 @@ -41,6 +41,11 @@ matching the current goal as introduction rule and not having "HOL." in their name (i.e. not being defined in theory HOL). +* Communication with Proof General is now 8bit clean, which means that +Unicode text in UTF-8 encoding may be used within theory texts (both +formal and informal parts). See option -U of the Isabelle Proof +General interface. + *** Document preparation *** @@ -224,29 +229,35 @@ *** Locales *** -* New commands for the interpretation of locale expressions in theories (1), -locales (2) and proof contexts (3). These generate proof obligations from -the expression specification. After the obligations have been discharged, -theorems of the expression are added to the theory, target locale or proof -context. The synopsis of the commands is a follows: +* New commands for the interpretation of locale expressions in +theories (1), locales (2) and proof contexts (3). These generate +proof obligations from the expression specification. After the +obligations have been discharged, theorems of the expression are added +to the theory, target locale or proof context. The synopsis of the +commands is a follows: + (1) interpretation expr inst (2) interpretation target < expr (3) interpret expr inst + Interpretation in theories and proof contexts require a parameter instantiation of terms from the current context. This is applied to -specifications and theorems of the interpreted expression. Interpretation -in locales only permits parameter renaming through the locale expression. -Interpretation is smart in that interpretations that are active already -do not occur in proof obligations, neither are instantiated theorems stored -in duplicate. Use 'print_interps' to inspect active interpretations of -a particular locale. For details, see the Isar Reference manual. +specifications and theorems of the interpreted expression. +Interpretation in locales only permits parameter renaming through the +locale expression. Interpretation is smart in that interpretations +that are active already do not occur in proof obligations, neither are +instantiated theorems stored in duplicate. Use 'print_interps' to +inspect active interpretations of a particular locale. For details, +see the Isar Reference manual. INCOMPATIBILITY: former 'instantiate' has been withdrawn, use 'interpret' instead. -* New context element 'constrains' for adding type constraints to parameters. - -* Context expressions: renaming of parameters with syntax redeclaration. +* New context element 'constrains' for adding type constraints to +parameters. + +* Context expressions: renaming of parameters with syntax +redeclaration. * Locale declaration: 'includes' disallowed.