NEWS
changeset 17385 4dcae6e62268
parent 17371 923ef4a8c672
child 17389 b4743198b939
equal deleted inserted replaced
17384:c01de5939f5b 17385:4dcae6e62268
    39 
    39 
    40 prints the last 100 theorems matching the pattern "(_::nat) + _ + _",
    40 prints the last 100 theorems matching the pattern "(_::nat) + _ + _",
    41 matching the current goal as introduction rule and not having "HOL."
    41 matching the current goal as introduction rule and not having "HOL."
    42 in their name (i.e. not being defined in theory HOL).
    42 in their name (i.e. not being defined in theory HOL).
    43 
    43 
       
    44 * Communication with Proof General is now 8bit clean, which means that
       
    45 Unicode text in UTF-8 encoding may be used within theory texts (both
       
    46 formal and informal parts).  See option -U of the Isabelle Proof
       
    47 General interface.
       
    48 
    44 
    49 
    45 *** Document preparation ***
    50 *** Document preparation ***
    46 
    51 
    47 * Commands 'display_drafts' and 'print_drafts' perform simple output
    52 * Commands 'display_drafts' and 'print_drafts' perform simple output
    48 of raw sources.  Only those symbols that do not require additional
    53 of raw sources.  Only those symbols that do not require additional
   222 theory development.
   227 theory development.
   223 
   228 
   224 
   229 
   225 *** Locales ***
   230 *** Locales ***
   226 
   231 
   227 * New commands for the interpretation of locale expressions in theories (1),
   232 * New commands for the interpretation of locale expressions in
   228 locales (2) and proof contexts (3).  These generate proof obligations from
   233 theories (1), locales (2) and proof contexts (3).  These generate
   229 the expression specification.  After the obligations have been discharged,
   234 proof obligations from the expression specification.  After the
   230 theorems of the expression are added to the theory, target locale or proof
   235 obligations have been discharged, theorems of the expression are added
   231 context.  The synopsis of the commands is a follows:
   236 to the theory, target locale or proof context.  The synopsis of the
       
   237 commands is a follows:
       
   238 
   232   (1) interpretation expr inst
   239   (1) interpretation expr inst
   233   (2) interpretation target < expr
   240   (2) interpretation target < expr
   234   (3) interpret expr inst
   241   (3) interpret expr inst
       
   242 
   235 Interpretation in theories and proof contexts require a parameter
   243 Interpretation in theories and proof contexts require a parameter
   236 instantiation of terms from the current context.  This is applied to
   244 instantiation of terms from the current context.  This is applied to
   237 specifications and theorems of the interpreted expression.  Interpretation
   245 specifications and theorems of the interpreted expression.
   238 in locales only permits parameter renaming through the locale expression.
   246 Interpretation in locales only permits parameter renaming through the
   239 Interpretation is smart in that interpretations that are active already
   247 locale expression.  Interpretation is smart in that interpretations
   240 do not occur in proof obligations, neither are instantiated theorems stored
   248 that are active already do not occur in proof obligations, neither are
   241 in duplicate.  Use 'print_interps' to inspect active interpretations of
   249 instantiated theorems stored in duplicate.  Use 'print_interps' to
   242 a particular locale.  For details, see the Isar Reference manual.
   250 inspect active interpretations of a particular locale.  For details,
       
   251 see the Isar Reference manual.
   243 
   252 
   244 INCOMPATIBILITY: former 'instantiate' has been withdrawn, use
   253 INCOMPATIBILITY: former 'instantiate' has been withdrawn, use
   245 'interpret' instead.
   254 'interpret' instead.
   246 
   255 
   247 * New context element 'constrains' for adding type constraints to parameters.
   256 * New context element 'constrains' for adding type constraints to
   248 
   257 parameters.
   249 * Context expressions: renaming of parameters with syntax redeclaration.
   258 
       
   259 * Context expressions: renaming of parameters with syntax
       
   260 redeclaration.
   250 
   261 
   251 * Locale declaration: 'includes' disallowed.
   262 * Locale declaration: 'includes' disallowed.
   252 
   263 
   253 * Proper static binding of attribute syntax -- i.e. types / terms /
   264 * Proper static binding of attribute syntax -- i.e. types / terms /
   254 facts mentioned as arguments are always those of the locale definition
   265 facts mentioned as arguments are always those of the locale definition