summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Mon, 10 May 2004 19:27:45 +0200 | |

changeset 14731 | 5670fc027a3b |

parent 14730 | 59ab60c6fcc6 |

child 14732 | 967db86e853c |

Pure: nested comments in inner syntax;

--- a/NEWS Mon May 10 19:26:58 2004 +0200 +++ b/NEWS Mon May 10 19:27:45 2004 +0200 @@ -7,55 +7,56 @@ *** General *** * Pure: considerably improved version of 'constdefs' command. Now -performs automatic type-inference of declared constants; additional -support for local structure declarations (cf. locales and HOL -records), see also isar-ref manual. Potential INCOMPATIBILITY: need -to observe strictly sequential dependencies of definitions within a -single 'constdefs' section; moreover, the declared name needs to be an -identifier. If all fails, consider to fall back on 'consts' and -'defs' separately. + performs automatic type-inference of declared constants; additional + support for local structure declarations (cf. locales and HOL + records), see also isar-ref manual. Potential INCOMPATIBILITY: need + to observe strictly sequential dependencies of definitions within a + single 'constdefs' section; moreover, the declared name needs to be + an identifier. If all fails, consider to fall back on 'consts' and + 'defs' separately. * Pure: improved indexed syntax and implicit structures. First of -all, indexed syntax provides a notational device for subscripted -application, using the new syntax \<^bsub>term\<^esub> for arbitrary -expressions. Secondly, in a local context with structure -declarations, number indexes \<^sub>n or the empty index (default -number 1) refer to a certain fixed variable implicitly; option -show_structs controls printing of implicit structures. Typical -applications of these concepts involve record types and locales. + all, indexed syntax provides a notational device for subscripted + application, using the new syntax \<^bsub>term\<^esub> for arbitrary + expressions. Secondly, in a local context with structure + declarations, number indexes \<^sub>n or the empty index (default + number 1) refer to a certain fixed variable implicitly; option + show_structs controls printing of implicit structures. Typical + applications of these concepts involve record types and locales. + +* Pure: syntax of terms, types etc. includes (*(*nested*) comments*). * Pure: 'advanced' translation functions (parse_translation etc.) may -depend on the signature of the theory context being presently used for -parsing/printing, see also isar-ref manual. + depend on the signature of the theory context being presently used + for parsing/printing, see also isar-ref manual. * Pure: tuned internal renaming of symbolic identifiers -- attach -primes instead of base 26 numbers. + primes instead of base 26 numbers. *** HOL *** - -* HOL/record: reimplementation of records. Improved scalability for records with -many fields, avoiding performance problems for type inference. Records are no -longer composed of nested field types, -but of nested extension types. Therefore the record type only grows -linear in the number of extensions and not in the number of fields. -The top-level (users) view on records is preserved. -Potential INCOMPATIBILITY only in strange cases, where the theory -depends on the old record representation. The type generated for -a record is called <record_name>_ext_type. - - -* Simplifier: "record_upd_simproc" for simplification of multiple record -updates enabled by default. -INCOMPATIBILITY: old proofs break occasionally, since simplification -is more powerful by default. +* HOL/record: reimplementation of records. Improved scalability for + records with many fields, avoiding performance problems for type + inference. Records are no longer composed of nested field types, but + of nested extension types. Therefore the record type only grows + linear in the number of extensions and not in the number of fields. + The top-level (users) view on records is preserved. Potential + INCOMPATIBILITY only in strange cases, where the theory depends on + the old record representation. The type generated for a record is + called <record_name>_ext_type. + +* Simplifier: "record_upd_simproc" for simplification of multiple + record updates enabled by default. INCOMPATIBILITY: old proofs + break occasionally, since simplification is more powerful by + default. + *** HOLCF *** * HOLCF: discontinued special version of 'constdefs' (which used to -support continuous functions) in favor of the general Pure one with -full type-inference. + support continuous functions) in favor of the general Pure one with + full type-inference. @@ -80,10 +81,10 @@ * Pure: Macintosh and Windows line-breaks are now allowed in theory files. -* Pure: single letter sub/superscripts (\<^isub> and \<^isup>) are now - allowed in identifiers. Similar to Greek letters \<^isub> is now considered - a normal (but invisible) letter. For multiple letter subscripts repeat - \<^isub> like this: x\<^isub>1\<^isub>2. +* Pure: single letter sub/superscripts (\<^isub> and \<^isup>) are now + allowed in identifiers. Similar to Greek letters \<^isub> is now considered + a normal (but invisible) letter. For multiple letter subscripts repeat + \<^isub> like this: x\<^isub>1\<^isub>2. * Pure: There are now sub-/superscripts that can span more than one character. Text between \<^bsub> and \<^esub> is set in subscript in @@ -104,7 +105,7 @@ (i.e. intersections of classes), * Presentation: generated HTML now uses a CSS style sheet to make layout - (somewhat) independent of content. It is copied from lib/html/isabelle.css. + (somewhat) independent of content. It is copied from lib/html/isabelle.css. It can be changed to alter the colors/layout of generated pages. @@ -174,15 +175,15 @@ of blast or auto after simplification become unnecessary because the goal is solved by simplification already. -* Numerics: new theory Ring_and_Field contains over 250 basic numerical laws, +* Numerics: new theory Ring_and_Field contains over 250 basic numerical laws, all proved in axiomatic type classes for semirings, rings and fields. * Numerics: - Numeric types (nat, int, and in HOL-Complex rat, real, complex, etc.) are - now formalized using the Ring_and_Field theory mentioned above. + now formalized using the Ring_and_Field theory mentioned above. - INCOMPATIBILITY: simplification and arithmetic behaves somewhat differently than before, because now they are set up once in a generic manner. - - INCOMPATIBILITY: many type-specific arithmetic laws have gone. + - INCOMPATIBILITY: many type-specific arithmetic laws have gone. Look for the general versions in Ring_and_Field (and Power if they concern exponentiation). @@ -192,12 +193,12 @@ - Record types are now by default printed with their type abbreviation instead of the list of all field types. This can be configured via the reference "print_record_type_abbr". - - Simproc "record_upd_simproc" for simplification of multiple updates added + - Simproc "record_upd_simproc" for simplification of multiple updates added (not enabled by default). - Simproc "record_ex_sel_eq_simproc" to simplify EX x. sel r = x resp. EX x. x = sel r to True (not enabled by default). - Tactic "record_split_simp_tac" to split and simplify records added. - + * 'specification' command added, allowing for definition by specification. There is also an 'ax_specification' command that introduces the new constants axiomatically. @@ -209,7 +210,7 @@ * HOL-ex: InductiveInvariant_examples illustrates advanced recursive function definitions, thanks to Sava Krsti\'{c} and John Matthews. -* HOL-Matrix: a first theory for matrices in HOL with an application of +* HOL-Matrix: a first theory for matrices in HOL with an application of matrix theory to linear programming. * Unions and Intersections: @@ -220,8 +221,8 @@ The subscript version is also accepted as input syntax. * Unions and Intersections over Intervals: - There is new short syntax "UN i<=n. A" for "UN i:{0..n}. A". There is - also an x-symbol version with subscripts "\<Union>\<^bsub>i <= n\<^esub>. A" + There is new short syntax "UN i<=n. A" for "UN i:{0..n}. A". There is + also an x-symbol version with subscripts "\<Union>\<^bsub>i <= n\<^esub>. A" like in normal math, and corresponding versions for < and for intersection. * ML: the legacy theory structures Int and List have been removed. They had @@ -364,7 +365,7 @@ - Calls full Presburger arithmetic (by Amine Chaieb) if quantifier-free linear arithmetic fails. This takes account of quantifiers and divisibility. - Presburger arithmetic can also be called explicitly via presburger(_tac). + Presburger arithmetic can also be called explicitly via presburger(_tac). * simp's arithmetic capabilities have been enhanced a bit: it now takes ~= in premises into account (by performing a case split); @@ -374,9 +375,9 @@ * New tactic "trans_tac" and method "trans" instantiate Provers/linorder.ML for axclasses "order" and "linorder" (predicates -"<=", "<" and "="). - -* function INCOMPATIBILITIES: Pi-sets have been redefined and moved from main +"<=", "<" and "="). + +* function INCOMPATIBILITIES: Pi-sets have been redefined and moved from main HOL to Library/FuncSet; constant "Fun.op o" is now called "Fun.comp"; * 'typedef' command has new option "open" to suppress the set @@ -402,13 +403,13 @@ * GroupTheory: deleted, since its material has been moved to Algebra; -* Complex: new directory of the complex numbers with numeric constants, -nonstandard complex numbers, and some complex analysis, standard and +* Complex: new directory of the complex numbers with numeric constants, +nonstandard complex numbers, and some complex analysis, standard and nonstandard (Jacques Fleuriot); * HOL-Complex: new image for analysis, replacing HOL-Real and HOL-Hyperreal; -* Hyperreal: introduced Gauge integration and hyperreal logarithms (Jacques +* Hyperreal: introduced Gauge integration and hyperreal logarithms (Jacques Fleuriot); * Real/HahnBanach: updated and adapted to locales; @@ -454,13 +455,13 @@ shift some page breaks in large documents. To get the old behaviour use \renewcommand{\isanewline}{\mbox{}\\\mbox{}} in root.tex. -* minimized dependencies of isabelle.sty and isabellesym.sty on +* minimized dependencies of isabelle.sty and isabellesym.sty on other packages * \<euro> now needs package babel/greek instead of marvosym (which broke \Rightarrow) -* normal size for \<zero>...\<nine> (uses \mathbf instead of +* normal size for \<zero>...\<nine> (uses \mathbf instead of textcomp package) @@ -708,9 +709,9 @@ * HOL: canonical cases/induct rules for n-tuples (n = 3..7); * HOL: consolidated and renamed several theories. In particular: - Ord.thy has been absorbed into HOL.thy - String.thy has been absorbed into List.thy - + Ord.thy has been absorbed into HOL.thy + String.thy has been absorbed into List.thy + * HOL: concrete setsum syntax "\<Sum>i:A. b" == "setsum (%i. b) A" (beware of argument permutation!);