1.1 --- a/NEWS Sat Apr 28 18:05:19 2012 +0200
1.2 +++ b/NEWS Sat Apr 28 18:09:50 2012 +0200
1.3 @@ -20,118 +20,50 @@
1.4 header -- minor INCOMPATIBILITY for user-defined commands. Allow new
1.5 commands to be used in the same theory where defined.
1.6
1.7 +* Auxiliary contexts indicate block structure for specifications with
1.8 +additional parameters and assumptions. Such unnamed contexts may be
1.9 +nested within other targets, like 'theory', 'locale', 'class',
1.10 +'instantiation' etc. Results from the local context are generalized
1.11 +accordingly and applied to the enclosing target context. Example:
1.12 +
1.13 + context
1.14 + fixes x y z :: 'a
1.15 + assumes xy: "x = y" and yz: "y = z"
1.16 + begin
1.17 +
1.18 + lemma my_trans: "x = z" using xy yz by simp
1.19 +
1.20 + end
1.21 +
1.22 + thm my_trans
1.23 +
1.24 +The most basic application is to factor-out context elements of
1.25 +several fixes/assumes/shows theorem statements, e.g. see
1.26 +~~/src/HOL/Isar_Examples/Group_Context.thy
1.27 +
1.28 +Any other local theory specification element works within the "context
1.29 +... begin ... end" block as well.
1.30 +
1.31 +* Bundled declarations associate attributed fact expressions with a
1.32 +given name in the context. These may be later included in other
1.33 +contexts. This allows to manage context extensions casually, without
1.34 +the logical dependencies of locales and locale interpretation.
1.35 +
1.36 +See commands 'bundle', 'include', 'including' etc. in the isar-ref
1.37 +manual.
1.38 +
1.39 +* Commands 'lemmas' and 'theorems' allow local variables using 'for'
1.40 +declaration, and results are standardized before being stored. Thus
1.41 +old-style "standard" after instantiation or composition of facts
1.42 +becomes obsolete. Minor INCOMPATIBILITY, due to potential change of
1.43 +indices of schematic variables.
1.44 +
1.45 * Rule attributes in local theory declarations (e.g. locale or class)
1.46 are now statically evaluated: the resulting theorem is stored instead
1.47 of the original expression. INCOMPATIBILITY in rare situations, where
1.48 the historic accident of dynamic re-evaluation in interpretations
1.49 etc. was exploited.
1.50
1.51 -* Commands 'lemmas' and 'theorems' allow local variables using 'for'
1.52 -declaration, and results are standardized before being stored. Thus
1.53 -old-style "standard" after instantiation or composition of facts
1.54 -becomes obsolete. Minor INCOMPATIBILITY, due to potential change of
1.55 -indices of schematic variables.
1.56 -
1.57 -* Simplified configuration options for syntax ambiguity: see
1.58 -"syntax_ambiguity_warning" and "syntax_ambiguity_limit" in isar-ref
1.59 -manual. Minor INCOMPATIBILITY.
1.60 -
1.61 -* Updated and extended reference manuals: "isar-ref",
1.62 -"implementation", "system"; reduced remaining material in old "ref"
1.63 -manual.
1.64 -
1.65 -
1.66 -*** Pure ***
1.67 -
1.68 -* Auxiliary contexts indicate block structure for specifications with
1.69 -additional parameters and assumptions. Such unnamed contexts may be
1.70 -nested within other targets, like 'theory', 'locale', 'class',
1.71 -'instantiation' etc. Results from the local context are generalized
1.72 -accordingly and applied to the enclosing target context. Example:
1.73 -
1.74 - context
1.75 - fixes x y z :: 'a
1.76 - assumes xy: "x = y" and yz: "y = z"
1.77 - begin
1.78 -
1.79 - lemma my_trans: "x = z" using xy yz by simp
1.80 -
1.81 - end
1.82 -
1.83 - thm my_trans
1.84 -
1.85 -The most basic application is to factor-out context elements of
1.86 -several fixes/assumes/shows theorem statements, e.g. see
1.87 -~~/src/HOL/Isar_Examples/Group_Context.thy
1.88 -
1.89 -Any other local theory specification element works within the "context
1.90 -... begin ... end" block as well.
1.91 -
1.92 -* Bundled declarations associate attributed fact expressions with a
1.93 -given name in the context. These may be later included in other
1.94 -contexts. This allows to manage context extensions casually, without
1.95 -the logical dependencies of locales and locale interpretation.
1.96 -
1.97 -See commands 'bundle', 'include', 'including' etc. in the isar-ref
1.98 -manual.
1.99 -
1.100 -* Rule composition via attribute "OF" (or ML functions OF/MRS) is more
1.101 -tolerant against multiple unifiers, as long as the final result is
1.102 -unique. (As before, rules are composed in canonical right-to-left
1.103 -order to accommodate newly introduced premises.)
1.104 -
1.105 -* Command 'definition' no longer exports the foundational "raw_def"
1.106 -into the user context. Minor INCOMPATIBILITY, may use the regular
1.107 -"def" result with attribute "abs_def" to imitate the old version.
1.108 -
1.109 -* Renamed some inner syntax categories:
1.110 -
1.111 - num ~> num_token
1.112 - xnum ~> xnum_token
1.113 - xstr ~> str_token
1.114 -
1.115 -Minor INCOMPATIBILITY. Note that in practice "num_const" or
1.116 -"num_position" etc. are mainly used instead (which also include
1.117 -position information via constraints).
1.118 -
1.119 -* Attribute "abs_def" turns an equation of the form "f x y == t" into
1.120 -"f == %x y. t", which ensures that "simp" or "unfold" steps always
1.121 -expand it. This also works for object-logic equality. (Formerly
1.122 -undocumented feature.)
1.123 -
1.124 -* Discontinued old "prems" fact, which used to refer to the accidental
1.125 -collection of foundational premises in the context (already marked as
1.126 -legacy since Isabelle2011).
1.127 -
1.128 -* Obsolete command 'types' has been discontinued. Use 'type_synonym'
1.129 -instead. INCOMPATIBILITY.
1.130 -
1.131 -* Old code generator for SML and its commands 'code_module',
1.132 -'code_library', 'consts_code', 'types_code' have been discontinued.
1.133 -Use commands of the generic code generator instead. INCOMPATIBILITY.
1.134 -
1.135 -* Redundant attribute "code_inline" has been discontinued. Use
1.136 -"code_unfold" instead. INCOMPATIBILITY.
1.137 -
1.138 -* Dropped attribute "code_unfold_post" in favor of the its dual
1.139 -"code_abbrev", which yields a common pattern in definitions like
1.140 -
1.141 - definition [code_abbrev]: "f = t"
1.142 -
1.143 -INCOMPATIBILITY.
1.144 -
1.145 -* Sort constraints are now propagated in simultaneous statements, just
1.146 -like type constraints. INCOMPATIBILITY in rare situations, where
1.147 -distinct sorts used to be assigned accidentally. For example:
1.148 -
1.149 - lemma "P (x::'a::foo)" and "Q (y::'a::bar)" -- "now illegal"
1.150 -
1.151 - lemma "P (x::'a)" and "Q (y::'a::bar)"
1.152 - -- "now uniform 'a::bar instead of default sort for first occurrence (!)"
1.153 -
1.154 -
1.155 -*** HOL ***
1.156 -
1.157 * New tutorial "Programming and Proving in Isabelle/HOL"
1.158 ("prog-prove"). It completely supersedes "A Tutorial Introduction to
1.159 Structured Isar Proofs" ("isar-overview"), which has been removed. It
1.160 @@ -139,6 +71,74 @@
1.161 Logic" as the recommended beginners tutorial, but does not cover all
1.162 of the material of that old tutorial.
1.163
1.164 +* Updated and extended reference manuals: "isar-ref",
1.165 +"implementation", "system"; reduced remaining material in old "ref"
1.166 +manual.
1.167 +
1.168 +
1.169 +*** Pure ***
1.170 +
1.171 +* Discontinued old "prems" fact, which used to refer to the accidental
1.172 +collection of foundational premises in the context (already marked as
1.173 +legacy since Isabelle2011).
1.174 +
1.175 +* Rule composition via attribute "OF" (or ML functions OF/MRS) is more
1.176 +tolerant against multiple unifiers, as long as the final result is
1.177 +unique. (As before, rules are composed in canonical right-to-left
1.178 +order to accommodate newly introduced premises.)
1.179 +
1.180 +* Command 'definition' no longer exports the foundational "raw_def"
1.181 +into the user context. Minor INCOMPATIBILITY, may use the regular
1.182 +"def" result with attribute "abs_def" to imitate the old version.
1.183 +
1.184 +* Renamed some inner syntax categories:
1.185 +
1.186 + num ~> num_token
1.187 + xnum ~> xnum_token
1.188 + xstr ~> str_token
1.189 +
1.190 +Minor INCOMPATIBILITY. Note that in practice "num_const" or
1.191 +"num_position" etc. are mainly used instead (which also include
1.192 +position information via constraints).
1.193 +
1.194 +* Simplified configuration options for syntax ambiguity: see
1.195 +"syntax_ambiguity_warning" and "syntax_ambiguity_limit" in isar-ref
1.196 +manual. Minor INCOMPATIBILITY.
1.197 +
1.198 +* Attribute "abs_def" turns an equation of the form "f x y == t" into
1.199 +"f == %x y. t", which ensures that "simp" or "unfold" steps always
1.200 +expand it. This also works for object-logic equality. (Formerly
1.201 +undocumented feature.)
1.202 +
1.203 +* Obsolete command 'types' has been discontinued. Use 'type_synonym'
1.204 +instead. INCOMPATIBILITY.
1.205 +
1.206 +* Old code generator for SML and its commands 'code_module',
1.207 +'code_library', 'consts_code', 'types_code' have been discontinued.
1.208 +Use commands of the generic code generator instead. INCOMPATIBILITY.
1.209 +
1.210 +* Redundant attribute "code_inline" has been discontinued. Use
1.211 +"code_unfold" instead. INCOMPATIBILITY.
1.212 +
1.213 +* Dropped attribute "code_unfold_post" in favor of the its dual
1.214 +"code_abbrev", which yields a common pattern in definitions like
1.215 +
1.216 + definition [code_abbrev]: "f = t"
1.217 +
1.218 +INCOMPATIBILITY.
1.219 +
1.220 +* Sort constraints are now propagated in simultaneous statements, just
1.221 +like type constraints. INCOMPATIBILITY in rare situations, where
1.222 +distinct sorts used to be assigned accidentally. For example:
1.223 +
1.224 + lemma "P (x::'a::foo)" and "Q (y::'a::bar)" -- "now illegal"
1.225 +
1.226 + lemma "P (x::'a)" and "Q (y::'a::bar)"
1.227 + -- "now uniform 'a::bar instead of default sort for first occurrence (!)"
1.228 +
1.229 +
1.230 +*** HOL ***
1.231 +
1.232 * Type 'a set is now a proper type constructor (just as before
1.233 Isabelle2008). Definitions mem_def and Collect_def have disappeared.
1.234 Non-trivial INCOMPATIBILITY. For developments keeping predicates and
1.235 @@ -180,10 +180,10 @@
1.236 * Code generation by default implements sets as container type rather
1.237 than predicates. INCOMPATIBILITY.
1.238
1.239 -* New proof import from HOL Light: Faster, simpler, and more scalable.
1.240 -Requires a proof bundle, which is available as an external component.
1.241 -Discontinued old (and mostly dead) Importer for HOL4 and HOL Light.
1.242 -INCOMPATIBILITY.
1.243 +* HOL-Import: Re-implementation from scratch is faster, simpler, and
1.244 +more scalable. Requires a proof bundle, which is available as an
1.245 +external component. Discontinued old (and mostly dead) Importer for
1.246 +HOL4 and HOL Light. INCOMPATIBILITY.
1.247
1.248 * New type synonym 'a rel = ('a * 'a) set
1.249