author | wenzelm |

Fri Apr 27 21:02:34 2012 +0200 (2012-04-27) | |

changeset 47806 | 7e009f4e9f47 |

parent 47805 | 5d283dca6104 |

child 47807 | befe55c8bbdc |

tuned;

1.1 --- a/NEWS Fri Apr 27 20:57:40 2012 +0200 1.2 +++ b/NEWS Fri Apr 27 21:02:34 2012 +0200 1.3 @@ -9,15 +9,16 @@ 1.4 * Prover IDE (PIDE) improvements: 1.5 1.6 - more robust Sledgehammer integration (as before the sledgehammer 1.7 - command line needs to be typed into the source buffer) 1.8 + command-line needs to be typed into the source buffer) 1.9 - markup for bound variables 1.10 - - markup for types of term variables (e.g. displayed as tooltips) 1.11 + - markup for types of term variables (displayed as tooltips) 1.12 - support for user-defined Isar commands within the running session 1.13 - improved support for Unicode outside original 16bit range 1.14 e.g. glyph for \<A> (thanks to jEdit 4.5.1) 1.15 1.16 -* Updated and extended reference manuals ("isar-ref" and 1.17 -"implementation"); reduced remaining material in old "ref" manual. 1.18 +* Forward declaration of outer syntax keywords within the theory 1.19 +header -- minor INCOMPATIBILITY for user-defined commands. Allow new 1.20 +commands to be used in the same theory where defined. 1.21 1.22 * Rule attributes in local theory declarations (e.g. locale or class) 1.23 are now statically evaluated: the resulting theorem is stored instead 1.24 @@ -31,23 +32,12 @@ 1.25 becomes obsolete. Minor INCOMPATIBILITY, due to potential change of 1.26 indices of schematic variables. 1.27 1.28 -* Renamed some inner syntax categories: 1.29 - 1.30 - num ~> num_token 1.31 - xnum ~> xnum_token 1.32 - xstr ~> str_token 1.33 - 1.34 -Minor INCOMPATIBILITY. Note that in practice "num_const" or 1.35 -"num_position" etc. are mainly used instead (which also include 1.36 -position information via constraints). 1.37 - 1.38 * Simplified configuration options for syntax ambiguity: see 1.39 "syntax_ambiguity_warning" and "syntax_ambiguity_limit" in isar-ref 1.40 manual. Minor INCOMPATIBILITY. 1.41 1.42 -* Forward declaration of outer syntax keywords within the theory 1.43 -header -- minor INCOMPATIBILITY for user-defined commands. Allow new 1.44 -commands to be used in the same theory where defined. 1.45 +* Updated and extended reference manuals: "isar-ref" and 1.46 +"implementation"; reduced remaining material in old "ref" manual. 1.47 1.48 1.49 *** Pure *** 1.50 @@ -93,6 +83,16 @@ 1.51 into the user context. Minor INCOMPATIBILITY, may use the regular 1.52 "def" result with attribute "abs_def" to imitate the old version. 1.53 1.54 +* Renamed some inner syntax categories: 1.55 + 1.56 + num ~> num_token 1.57 + xnum ~> xnum_token 1.58 + xstr ~> str_token 1.59 + 1.60 +Minor INCOMPATIBILITY. Note that in practice "num_const" or 1.61 +"num_position" etc. are mainly used instead (which also include 1.62 +position information via constraints). 1.63 + 1.64 * Attribute "abs_def" turns an equation of the form "f x y == t" into 1.65 "f == %x y. t", which ensures that "simp" or "unfold" steps always 1.66 expand it. This also works for object-logic equality. (Formerly 1.67 @@ -131,13 +131,12 @@ 1.68 1.69 *** HOL *** 1.70 1.71 -* New tutorial "Programming and Proving in Isabelle/HOL" ("prog-prove"). 1.72 -It completely supercedes "A Tutorial Introduction to Structured Isar Proofs", 1.73 -which has been removed. It supercedes "Isabelle/HOL, A Proof Assistant 1.74 -for Higher-Order Logic" as the recommended beginners tutorial 1.75 -but does not cover all of the material of that old tutorial. 1.76 - 1.77 -* Discontinued old Tutorial on Isar ("isar-overview"); 1.78 +* New tutorial "Programming and Proving in Isabelle/HOL" 1.79 +("prog-prove"). It completely supersedes "A Tutorial Introduction to 1.80 +Structured Isar Proofs" ("isar-overview"), which has been removed. It 1.81 +also supersedes "Isabelle/HOL, A Proof Assistant for Higher-Order 1.82 +Logic" as the recommended beginners tutorial, but does not cover all 1.83 +of the material of that old tutorial. 1.84 1.85 * Type 'a set is now a proper type constructor (just as before 1.86 Isabelle2008). Definitions mem_def and Collect_def have disappeared.