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

author | wenzelm |

Tue, 19 Jan 2016 14:00:47 +0100 | |

changeset 62205 | ca68dc26fbb6 |

parent 62204 | 7f5579b12b0a |

child 62206 | aed720a91f2f |

tuned;

CONTRIBUTORS | file | annotate | diff | comparison | revisions | |

NEWS | file | annotate | diff | comparison | revisions |

--- a/CONTRIBUTORS Tue Jan 19 11:46:54 2016 +0100 +++ b/CONTRIBUTORS Tue Jan 19 14:00:47 2016 +0100 @@ -16,10 +16,10 @@ * Summer 2015 - Winter 2016: Lawrence C Paulson, Cambridge General, homology form of Cauchy's integral theorem and supporting material - (ported from HOL Light) + (ported from HOL Light). * Winter 2015/16: Gerwin Klein, NICTA - print_record command + New print_record command. * Winter 2015: Manuel Eberl, TUM The radius of convergence of power series and various summability tests.

--- a/NEWS Tue Jan 19 11:46:54 2016 +0100 +++ b/NEWS Tue Jan 19 14:00:47 2016 +0100 @@ -194,9 +194,9 @@ *** Isar *** -* Local goals ('have', 'show', 'hence', 'thus') allow structured -rule statements like fixes/assumes/shows in theorem specifications, but -the notation is postfix with keywords 'if' (or 'when') and 'for'. For +* Local goals ('have', 'show', 'hence', 'thus') allow structured rule +statements like fixes/assumes/shows in theorem specifications, but the +notation is postfix with keywords 'if' (or 'when') and 'for'. For example: have result: "C x y" @@ -240,7 +240,8 @@ * The meaning of 'show' with Pure rule statements has changed: premises are treated in the sense of 'assume', instead of 'presume'. This means, -a goal like "\<And>x. A x \<Longrightarrow> B x \<Longrightarrow> C x" can be solved completely as follows: +a goal like "\<And>x. A x \<Longrightarrow> B x \<Longrightarrow> C x" can be solved completely as +follows: show "\<And>x. A x \<Longrightarrow> B x \<Longrightarrow> C x" @@ -401,12 +402,12 @@ * Configuration option rule_insts_schematic has been discontinued (intermediate legacy feature in Isabelle2015). INCOMPATIBILITY. -* Abbreviations in type classes now carry proper sort constraint. -Rare INCOMPATIBILITY in situations where the previous misbehaviour -has been exploited. +* Abbreviations in type classes now carry proper sort constraint. Rare +INCOMPATIBILITY in situations where the previous misbehaviour has been +exploited. * Refinement of user-space type system in type classes: pseudo-local -operations behave more similar to abbreviations. Potential +operations behave more similar to abbreviations. Potential INCOMPATIBILITY in exotic situations. @@ -471,7 +472,8 @@ * Recursive function definitions ('fun', 'function', 'partial_function') expose low-level facts of the internal construction only if the option -"function_internals" is enabled. Rare INCOMPATIBILITY. +"function_internals" is enabled. Its internal inductive definition is +also subject to "inductive_internals". Rare INCOMPATIBILITY. * BNF datatypes ('datatype', 'codatatype', etc.) expose low-level facts of the internal construction only if the option "bnf_internals" is @@ -635,8 +637,8 @@ * Class uniform_space introduces uniform spaces btw topological spaces and metric spaces. Minor INCOMPATIBILITY: open_<type>_def needs to be -introduced in the form of an uniformity. Some constants are more -general now, it may be necessary to add type class constraints. +introduced in the form of an uniformity. Some constants are more general +now, it may be necessary to add type class constraints. open_real_def \<leadsto> open_dist open_complex_def \<leadsto> open_dist @@ -794,7 +796,7 @@ performance. * Property values in etc/symbols may contain spaces, if written with the -replacement character "␣" (Unicode point 0x2324). For example: +replacement character "␣" (Unicode point 0x2324). For example: \<star> code: 0x0022c6 group: operator font: Deja␣Vu␣Sans␣Mono @@ -818,8 +820,8 @@ is relevant both for Poly/ML and JVM processes. * Poly/ML default platform architecture may be changed from 32bit to -64bit via system option ML_system_64. A system restart (and rebuild) -is required after change. +64bit via system option ML_system_64. A system restart (and rebuild) is +required after change. * Poly/ML 5.6 runs natively on x86-windows and x86_64-windows, which both allow larger heap space than former x86-cygwin.