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