summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

NEWS

changeset 14731 | 5670fc027a3b |

parent 14709 | d01983034ded |

child 14795 | b702848de41f |

1.1 --- a/NEWS Mon May 10 19:26:58 2004 +0200 1.2 +++ b/NEWS Mon May 10 19:27:45 2004 +0200 1.3 @@ -7,55 +7,56 @@ 1.4 *** General *** 1.5 1.6 * Pure: considerably improved version of 'constdefs' command. Now 1.7 -performs automatic type-inference of declared constants; additional 1.8 -support for local structure declarations (cf. locales and HOL 1.9 -records), see also isar-ref manual. Potential INCOMPATIBILITY: need 1.10 -to observe strictly sequential dependencies of definitions within a 1.11 -single 'constdefs' section; moreover, the declared name needs to be an 1.12 -identifier. If all fails, consider to fall back on 'consts' and 1.13 -'defs' separately. 1.14 + performs automatic type-inference of declared constants; additional 1.15 + support for local structure declarations (cf. locales and HOL 1.16 + records), see also isar-ref manual. Potential INCOMPATIBILITY: need 1.17 + to observe strictly sequential dependencies of definitions within a 1.18 + single 'constdefs' section; moreover, the declared name needs to be 1.19 + an identifier. If all fails, consider to fall back on 'consts' and 1.20 + 'defs' separately. 1.21 1.22 * Pure: improved indexed syntax and implicit structures. First of 1.23 -all, indexed syntax provides a notational device for subscripted 1.24 -application, using the new syntax \<^bsub>term\<^esub> for arbitrary 1.25 -expressions. Secondly, in a local context with structure 1.26 -declarations, number indexes \<^sub>n or the empty index (default 1.27 -number 1) refer to a certain fixed variable implicitly; option 1.28 -show_structs controls printing of implicit structures. Typical 1.29 -applications of these concepts involve record types and locales. 1.30 + all, indexed syntax provides a notational device for subscripted 1.31 + application, using the new syntax \<^bsub>term\<^esub> for arbitrary 1.32 + expressions. Secondly, in a local context with structure 1.33 + declarations, number indexes \<^sub>n or the empty index (default 1.34 + number 1) refer to a certain fixed variable implicitly; option 1.35 + show_structs controls printing of implicit structures. Typical 1.36 + applications of these concepts involve record types and locales. 1.37 + 1.38 +* Pure: syntax of terms, types etc. includes (*(*nested*) comments*). 1.39 1.40 * Pure: 'advanced' translation functions (parse_translation etc.) may 1.41 -depend on the signature of the theory context being presently used for 1.42 -parsing/printing, see also isar-ref manual. 1.43 + depend on the signature of the theory context being presently used 1.44 + for parsing/printing, see also isar-ref manual. 1.45 1.46 * Pure: tuned internal renaming of symbolic identifiers -- attach 1.47 -primes instead of base 26 numbers. 1.48 + primes instead of base 26 numbers. 1.49 1.50 1.51 *** HOL *** 1.52 1.53 - 1.54 -* HOL/record: reimplementation of records. Improved scalability for records with 1.55 -many fields, avoiding performance problems for type inference. Records are no 1.56 -longer composed of nested field types, 1.57 -but of nested extension types. Therefore the record type only grows 1.58 -linear in the number of extensions and not in the number of fields. 1.59 -The top-level (users) view on records is preserved. 1.60 -Potential INCOMPATIBILITY only in strange cases, where the theory 1.61 -depends on the old record representation. The type generated for 1.62 -a record is called <record_name>_ext_type. 1.63 - 1.64 - 1.65 -* Simplifier: "record_upd_simproc" for simplification of multiple record 1.66 -updates enabled by default. 1.67 -INCOMPATIBILITY: old proofs break occasionally, since simplification 1.68 -is more powerful by default. 1.69 +* HOL/record: reimplementation of records. Improved scalability for 1.70 + records with many fields, avoiding performance problems for type 1.71 + inference. Records are no longer composed of nested field types, but 1.72 + of nested extension types. Therefore the record type only grows 1.73 + linear in the number of extensions and not in the number of fields. 1.74 + The top-level (users) view on records is preserved. Potential 1.75 + INCOMPATIBILITY only in strange cases, where the theory depends on 1.76 + the old record representation. The type generated for a record is 1.77 + called <record_name>_ext_type. 1.78 + 1.79 +* Simplifier: "record_upd_simproc" for simplification of multiple 1.80 + record updates enabled by default. INCOMPATIBILITY: old proofs 1.81 + break occasionally, since simplification is more powerful by 1.82 + default. 1.83 + 1.84 1.85 *** HOLCF *** 1.86 1.87 * HOLCF: discontinued special version of 'constdefs' (which used to 1.88 -support continuous functions) in favor of the general Pure one with 1.89 -full type-inference. 1.90 + support continuous functions) in favor of the general Pure one with 1.91 + full type-inference. 1.92 1.93 1.94 1.95 @@ -80,10 +81,10 @@ 1.96 1.97 * Pure: Macintosh and Windows line-breaks are now allowed in theory files. 1.98 1.99 -* Pure: single letter sub/superscripts (\<^isub> and \<^isup>) are now 1.100 - allowed in identifiers. Similar to Greek letters \<^isub> is now considered 1.101 - a normal (but invisible) letter. For multiple letter subscripts repeat 1.102 - \<^isub> like this: x\<^isub>1\<^isub>2. 1.103 +* Pure: single letter sub/superscripts (\<^isub> and \<^isup>) are now 1.104 + allowed in identifiers. Similar to Greek letters \<^isub> is now considered 1.105 + a normal (but invisible) letter. For multiple letter subscripts repeat 1.106 + \<^isub> like this: x\<^isub>1\<^isub>2. 1.107 1.108 * Pure: There are now sub-/superscripts that can span more than one 1.109 character. Text between \<^bsub> and \<^esub> is set in subscript in 1.110 @@ -104,7 +105,7 @@ 1.111 (i.e. intersections of classes), 1.112 1.113 * Presentation: generated HTML now uses a CSS style sheet to make layout 1.114 - (somewhat) independent of content. It is copied from lib/html/isabelle.css. 1.115 + (somewhat) independent of content. It is copied from lib/html/isabelle.css. 1.116 It can be changed to alter the colors/layout of generated pages. 1.117 1.118 1.119 @@ -174,15 +175,15 @@ 1.120 of blast or auto after simplification become unnecessary because the goal 1.121 is solved by simplification already. 1.122 1.123 -* Numerics: new theory Ring_and_Field contains over 250 basic numerical laws, 1.124 +* Numerics: new theory Ring_and_Field contains over 250 basic numerical laws, 1.125 all proved in axiomatic type classes for semirings, rings and fields. 1.126 1.127 * Numerics: 1.128 - Numeric types (nat, int, and in HOL-Complex rat, real, complex, etc.) are 1.129 - now formalized using the Ring_and_Field theory mentioned above. 1.130 + now formalized using the Ring_and_Field theory mentioned above. 1.131 - INCOMPATIBILITY: simplification and arithmetic behaves somewhat differently 1.132 than before, because now they are set up once in a generic manner. 1.133 - - INCOMPATIBILITY: many type-specific arithmetic laws have gone. 1.134 + - INCOMPATIBILITY: many type-specific arithmetic laws have gone. 1.135 Look for the general versions in Ring_and_Field (and Power if they concern 1.136 exponentiation). 1.137 1.138 @@ -192,12 +193,12 @@ 1.139 - Record types are now by default printed with their type abbreviation 1.140 instead of the list of all field types. This can be configured via 1.141 the reference "print_record_type_abbr". 1.142 - - Simproc "record_upd_simproc" for simplification of multiple updates added 1.143 + - Simproc "record_upd_simproc" for simplification of multiple updates added 1.144 (not enabled by default). 1.145 - Simproc "record_ex_sel_eq_simproc" to simplify EX x. sel r = x resp. 1.146 EX x. x = sel r to True (not enabled by default). 1.147 - Tactic "record_split_simp_tac" to split and simplify records added. 1.148 - 1.149 + 1.150 * 'specification' command added, allowing for definition by 1.151 specification. There is also an 'ax_specification' command that 1.152 introduces the new constants axiomatically. 1.153 @@ -209,7 +210,7 @@ 1.154 * HOL-ex: InductiveInvariant_examples illustrates advanced recursive function 1.155 definitions, thanks to Sava Krsti\'{c} and John Matthews. 1.156 1.157 -* HOL-Matrix: a first theory for matrices in HOL with an application of 1.158 +* HOL-Matrix: a first theory for matrices in HOL with an application of 1.159 matrix theory to linear programming. 1.160 1.161 * Unions and Intersections: 1.162 @@ -220,8 +221,8 @@ 1.163 The subscript version is also accepted as input syntax. 1.164 1.165 * Unions and Intersections over Intervals: 1.166 - There is new short syntax "UN i<=n. A" for "UN i:{0..n}. A". There is 1.167 - also an x-symbol version with subscripts "\<Union>\<^bsub>i <= n\<^esub>. A" 1.168 + There is new short syntax "UN i<=n. A" for "UN i:{0..n}. A". There is 1.169 + also an x-symbol version with subscripts "\<Union>\<^bsub>i <= n\<^esub>. A" 1.170 like in normal math, and corresponding versions for < and for intersection. 1.171 1.172 * ML: the legacy theory structures Int and List have been removed. They had 1.173 @@ -364,7 +365,7 @@ 1.174 1.175 - Calls full Presburger arithmetic (by Amine Chaieb) if quantifier-free 1.176 linear arithmetic fails. This takes account of quantifiers and divisibility. 1.177 - Presburger arithmetic can also be called explicitly via presburger(_tac). 1.178 + Presburger arithmetic can also be called explicitly via presburger(_tac). 1.179 1.180 * simp's arithmetic capabilities have been enhanced a bit: it now 1.181 takes ~= in premises into account (by performing a case split); 1.182 @@ -374,9 +375,9 @@ 1.183 1.184 * New tactic "trans_tac" and method "trans" instantiate 1.185 Provers/linorder.ML for axclasses "order" and "linorder" (predicates 1.186 -"<=", "<" and "="). 1.187 - 1.188 -* function INCOMPATIBILITIES: Pi-sets have been redefined and moved from main 1.189 +"<=", "<" and "="). 1.190 + 1.191 +* function INCOMPATIBILITIES: Pi-sets have been redefined and moved from main 1.192 HOL to Library/FuncSet; constant "Fun.op o" is now called "Fun.comp"; 1.193 1.194 * 'typedef' command has new option "open" to suppress the set 1.195 @@ -402,13 +403,13 @@ 1.196 1.197 * GroupTheory: deleted, since its material has been moved to Algebra; 1.198 1.199 -* Complex: new directory of the complex numbers with numeric constants, 1.200 -nonstandard complex numbers, and some complex analysis, standard and 1.201 +* Complex: new directory of the complex numbers with numeric constants, 1.202 +nonstandard complex numbers, and some complex analysis, standard and 1.203 nonstandard (Jacques Fleuriot); 1.204 1.205 * HOL-Complex: new image for analysis, replacing HOL-Real and HOL-Hyperreal; 1.206 1.207 -* Hyperreal: introduced Gauge integration and hyperreal logarithms (Jacques 1.208 +* Hyperreal: introduced Gauge integration and hyperreal logarithms (Jacques 1.209 Fleuriot); 1.210 1.211 * Real/HahnBanach: updated and adapted to locales; 1.212 @@ -454,13 +455,13 @@ 1.213 shift some page breaks in large documents. To get the old behaviour 1.214 use \renewcommand{\isanewline}{\mbox{}\\\mbox{}} in root.tex. 1.215 1.216 -* minimized dependencies of isabelle.sty and isabellesym.sty on 1.217 +* minimized dependencies of isabelle.sty and isabellesym.sty on 1.218 other packages 1.219 1.220 * \<euro> now needs package babel/greek instead of marvosym (which 1.221 broke \Rightarrow) 1.222 1.223 -* normal size for \<zero>...\<nine> (uses \mathbf instead of 1.224 +* normal size for \<zero>...\<nine> (uses \mathbf instead of 1.225 textcomp package) 1.226 1.227 1.228 @@ -708,9 +709,9 @@ 1.229 * HOL: canonical cases/induct rules for n-tuples (n = 3..7); 1.230 1.231 * HOL: consolidated and renamed several theories. In particular: 1.232 - Ord.thy has been absorbed into HOL.thy 1.233 - String.thy has been absorbed into List.thy 1.234 - 1.235 + Ord.thy has been absorbed into HOL.thy 1.236 + String.thy has been absorbed into List.thy 1.237 + 1.238 * HOL: concrete setsum syntax "\<Sum>i:A. b" == "setsum (%i. b) A" 1.239 (beware of argument permutation!); 1.240