interpretation/interpret: prefixes are mandatory by default;
authorwenzelm
Thu Mar 26 19:24:21 2009 +0100 (2009-03-26)
changeset 30728f0aeca99b5d9
parent 30727 519f8f0fcbf3
child 30729 461ee3e49ad3
interpretation/interpret: prefixes are mandatory by default;
misc tuning and updates;
NEWS
     1.1 --- a/NEWS	Thu Mar 26 19:00:29 2009 +0100
     1.2 +++ b/NEWS	Thu Mar 26 19:24:21 2009 +0100
     1.3 @@ -139,8 +139,8 @@
     1.4  INCOMPATBILITY.
     1.5  
     1.6  * Complete re-implementation of locales.  INCOMPATIBILITY.  The most
     1.7 -important changes are listed below.  See documentation (forthcoming)
     1.8 -and tutorial (also forthcoming) for details.
     1.9 +important changes are listed below.  See the Tutorial on Locales for
    1.10 +details.
    1.11  
    1.12  - In locale expressions, instantiation replaces renaming.  Parameters
    1.13  must be declared in a for clause.  To aid compatibility with previous
    1.14 @@ -154,19 +154,23 @@
    1.15  
    1.16  - More flexible mechanisms to qualify names generated by locale
    1.17  expressions.  Qualifiers (prefixes) may be specified in locale
    1.18 -expressions.  Available are normal qualifiers (syntax "name:") and
    1.19 -strict qualifiers (syntax "name!:").  The latter must occur in name
    1.20 -references and are useful to avoid accidental hiding of names, the
    1.21 -former are optional.  Qualifiers derived from the parameter names of a
    1.22 -locale are no longer generated.
    1.23 +expressions, and can be marked as mandatory (syntax: "name!:") or
    1.24 +optional (syntax "name?:").  The default depends for plain "name:"
    1.25 +depends on the situation where a locale expression is used: in
    1.26 +commands 'locale' and 'sublocale' prefixes are optional, in
    1.27 +'interpretation' and 'interpret' prefixes are mandatory.  Old-style
    1.28 +implicit qualifiers derived from the parameter names of a locale are
    1.29 +no longer generated.
    1.30  
    1.31  - "sublocale l < e" replaces "interpretation l < e".  The
    1.32  instantiation clause in "interpretation" and "interpret" (square
    1.33  brackets) is no longer available.  Use locale expressions.
    1.34  
    1.35 -- When converting proof scripts, be sure to replace qualifiers in
    1.36 -"interpretation" and "interpret" by strict qualifiers.  Qualifiers in
    1.37 -locale expressions range over a single locale instance only.
    1.38 +- When converting proof scripts, be sure to mandatory qualifiers in
    1.39 +'interpretation' and 'interpret' should be retained by default, even
    1.40 +if this is an INCOMPATIBILITY compared to former behaviour.
    1.41 +Qualifiers in locale expressions range over a single locale instance
    1.42 +only.
    1.43  
    1.44  * Command 'instance': attached definitions no longer accepted.
    1.45  INCOMPATIBILITY, use proper 'instantiation' target.
    1.46 @@ -180,9 +184,9 @@
    1.47  directly solve the current goal.
    1.48  
    1.49  * Auto solve feature for main theorem statements (cf. option in Proof
    1.50 -General Isabelle settings menu, enabled by default).  Whenever a new
    1.51 +General Isabelle settings menu, disabled by default).  Whenever a new
    1.52  goal is stated, "find_theorems solves" is called; any theorems that
    1.53 -could solve the lemma directly are listed underneath the goal.
    1.54 +could solve the lemma directly are listed as part of the goal state.
    1.55  
    1.56  * Command 'find_consts' searches for constants based on type and name
    1.57  patterns, e.g.
    1.58 @@ -190,7 +194,7 @@
    1.59      find_consts "_ => bool"
    1.60  
    1.61  By default, matching is against subtypes, but it may be restricted to
    1.62 -the whole type. Searching by name is possible.  Multiple queries are
    1.63 +the whole type.  Searching by name is possible.  Multiple queries are
    1.64  conjunctive and queries may be negated by prefixing them with a
    1.65  hyphen:
    1.66