tuned;
authorwenzelm
Tue Jan 19 14:00:47 2016 +0100 (2016-01-19)
changeset 62205ca68dc26fbb6
parent 62204 7f5579b12b0a
child 62206 aed720a91f2f
tuned;
CONTRIBUTORS
NEWS
     1.1 --- a/CONTRIBUTORS	Tue Jan 19 11:46:54 2016 +0100
     1.2 +++ b/CONTRIBUTORS	Tue Jan 19 14:00:47 2016 +0100
     1.3 @@ -16,10 +16,10 @@
     1.4  
     1.5  * Summer 2015 - Winter 2016: Lawrence C Paulson, Cambridge
     1.6    General, homology form of Cauchy's integral theorem and supporting material
     1.7 -  (ported from HOL Light)
     1.8 +  (ported from HOL Light).
     1.9  
    1.10  * Winter 2015/16: Gerwin Klein, NICTA
    1.11 -  print_record command
    1.12 +  New print_record command.
    1.13  
    1.14  * Winter 2015: Manuel Eberl, TUM
    1.15    The radius of convergence of power series and various summability tests.
     2.1 --- a/NEWS	Tue Jan 19 11:46:54 2016 +0100
     2.2 +++ b/NEWS	Tue Jan 19 14:00:47 2016 +0100
     2.3 @@ -194,9 +194,9 @@
     2.4  
     2.5  *** Isar ***
     2.6  
     2.7 -* Local goals ('have', 'show', 'hence', 'thus') allow structured
     2.8 -rule statements like fixes/assumes/shows in theorem specifications, but
     2.9 -the notation is postfix with keywords 'if' (or 'when') and 'for'. For
    2.10 +* Local goals ('have', 'show', 'hence', 'thus') allow structured rule
    2.11 +statements like fixes/assumes/shows in theorem specifications, but the
    2.12 +notation is postfix with keywords 'if' (or 'when') and 'for'. For
    2.13  example:
    2.14  
    2.15    have result: "C x y"
    2.16 @@ -240,7 +240,8 @@
    2.17  
    2.18  * The meaning of 'show' with Pure rule statements has changed: premises
    2.19  are treated in the sense of 'assume', instead of 'presume'. This means,
    2.20 -a goal like "\<And>x. A x \<Longrightarrow> B x \<Longrightarrow> C x" can be solved completely as follows:
    2.21 +a goal like "\<And>x. A x \<Longrightarrow> B x \<Longrightarrow> C x" can be solved completely as
    2.22 +follows:
    2.23  
    2.24    show "\<And>x. A x \<Longrightarrow> B x \<Longrightarrow> C x"
    2.25  
    2.26 @@ -401,12 +402,12 @@
    2.27  * Configuration option rule_insts_schematic has been discontinued
    2.28  (intermediate legacy feature in Isabelle2015). INCOMPATIBILITY.
    2.29  
    2.30 -* Abbreviations in type classes now carry proper sort constraint.
    2.31 -Rare INCOMPATIBILITY in situations where the previous misbehaviour
    2.32 -has been exploited.
    2.33 +* Abbreviations in type classes now carry proper sort constraint. Rare
    2.34 +INCOMPATIBILITY in situations where the previous misbehaviour has been
    2.35 +exploited.
    2.36  
    2.37  * Refinement of user-space type system in type classes: pseudo-local
    2.38 -operations behave more similar to abbreviations.  Potential
    2.39 +operations behave more similar to abbreviations. Potential
    2.40  INCOMPATIBILITY in exotic situations.
    2.41  
    2.42  
    2.43 @@ -471,7 +472,8 @@
    2.44  
    2.45  * Recursive function definitions ('fun', 'function', 'partial_function')
    2.46  expose low-level facts of the internal construction only if the option
    2.47 -"function_internals" is enabled. Rare INCOMPATIBILITY.
    2.48 +"function_internals" is enabled. Its internal inductive definition is
    2.49 +also subject to "inductive_internals". Rare INCOMPATIBILITY.
    2.50  
    2.51  * BNF datatypes ('datatype', 'codatatype', etc.) expose low-level facts
    2.52  of the internal construction only if the option "bnf_internals" is
    2.53 @@ -635,8 +637,8 @@
    2.54  
    2.55  * Class uniform_space introduces uniform spaces btw topological spaces
    2.56  and metric spaces. Minor INCOMPATIBILITY: open_<type>_def needs to be
    2.57 -introduced in the form of an uniformity. Some constants are more
    2.58 -general now, it may be necessary to add type class constraints.
    2.59 +introduced in the form of an uniformity. Some constants are more general
    2.60 +now, it may be necessary to add type class constraints.
    2.61  
    2.62    open_real_def \<leadsto> open_dist
    2.63    open_complex_def \<leadsto> open_dist
    2.64 @@ -794,7 +796,7 @@
    2.65  performance.
    2.66  
    2.67  * Property values in etc/symbols may contain spaces, if written with the
    2.68 -replacement character "␣" (Unicode point 0x2324).  For example:
    2.69 +replacement character "␣" (Unicode point 0x2324). For example:
    2.70  
    2.71      \<star>  code: 0x0022c6  group: operator  font: Deja␣Vu␣Sans␣Mono
    2.72  
    2.73 @@ -818,8 +820,8 @@
    2.74  is relevant both for Poly/ML and JVM processes.
    2.75  
    2.76  * Poly/ML default platform architecture may be changed from 32bit to
    2.77 -64bit via system option ML_system_64. A system restart (and rebuild)
    2.78 -is required after change.
    2.79 +64bit via system option ML_system_64. A system restart (and rebuild) is
    2.80 +required after change.
    2.81  
    2.82  * Poly/ML 5.6 runs natively on x86-windows and x86_64-windows, which
    2.83  both allow larger heap space than former x86-cygwin.