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