summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

NEWS

changeset 22845 | 5f9138bcb3d7 |

parent 22826 | 0f4c501a691e |

child 22848 | f65a76867179 |

1.1 --- a/NEWS Sun May 06 21:49:44 2007 +0200 1.2 +++ b/NEWS Sun May 06 21:50:17 2007 +0200 1.3 @@ -95,10 +95,10 @@ 1.4 1.5 Theorem attributs for selecting and transforming function equations theorems: 1.6 1.7 - [code fun]: select a theorem as function equation for a specific constant 1.8 - [code nofun]: deselect a theorem as function equation for a specific constant 1.9 - [code inline]: select an equation theorem for unfolding (inlining) in place 1.10 - [code noinline]: deselect an equation theorem for unfolding (inlining) in place 1.11 + [code fun]: select a theorem as function equation for a specific constant 1.12 + [code fun del]: deselect a theorem as function equation for a specific constant 1.13 + [code inline]: select an equation theorem for unfolding (inlining) in place 1.14 + [code inline del]: deselect an equation theorem for unfolding (inlining) in place 1.15 1.16 User-defined serializations (target in {SML, OCaml, Haskell}): 1.17 1.18 @@ -519,6 +519,13 @@ 1.19 1.20 *** HOL *** 1.21 1.22 +* case expressions and primrec: missing cases now mapped to "undefined" 1.23 +instead of "arbitrary" 1.24 + 1.25 +* new constant "undefined" with axiom "undefined x = undefined" 1.26 + 1.27 +* new class "default" with associated constant "default" 1.28 + 1.29 * Library/Pretty_Int.thy: maps HOL numerals on target language integer literals 1.30 when generating code. 1.31 1.32 @@ -639,11 +646,11 @@ 1.33 meet_min ~> inf_min 1.34 join_max ~> sup_max 1.35 1.36 -* Class (axclass + locale) "preorder" and "linear": facts "refl", "trans" and 1.37 +* Classes "order" and "linorder": facts "refl", "trans" and 1.38 "cases" renamed ro "order_refl", "order_trans" and "linorder_cases", to 1.39 avoid clashes with HOL "refl" and "trans". INCOMPATIBILITY. 1.40 1.41 -* Addes class (axclass + locale) "preorder" as superclass of "order"; 1.42 +* Classes "order" and "linorder": 1.43 potential INCOMPATIBILITY: order of proof goals in order/linorder instance 1.44 proofs changed. 1.45