removed pred;
authorwenzelm
Mon Mar 09 16:30:55 1998 +0100 (1998-03-09)
changeset 471175a9ef36b1fe
parent 4710 05e57f1879ee
child 4712 facfbbca7242
removed pred;
NEWS
src/HOL/Arith.thy
     1.1 --- a/NEWS	Mon Mar 09 16:17:28 1998 +0100
     1.2 +++ b/NEWS	Mon Mar 09 16:30:55 1998 +0100
     1.3 @@ -9,7 +9,7 @@
     1.4    default simpset using Addsplits just like Addsimps. They can be removed via
     1.5    Delsplits just like Delsimps. For applications see HOL below.
     1.6  
     1.7 -* changed wrapper mechanism for the classical reasoner now allows for selected
     1.8 +* Changed wrapper mechanism for the classical reasoner now allows for selected
     1.9    deletion of wrappers, by introduction of names for wrapper functionals.
    1.10    This implies that addbefore, addSbefore, addaltern, and addSaltern now take
    1.11    a pair (name, tactic) as argument, and that adding two tactics with the same
    1.12 @@ -19,8 +19,11 @@
    1.13    delWrapper, delSWrapper: claset *  string -> claset
    1.14    getWrapper is renamed to appWrappers, getSWrapper to appSWrappers;
    1.15  
    1.16 +
    1.17  *** HOL ***
    1.18  
    1.19 +* HOL/Arithmetic: removed 'pred' (predecessor) function;
    1.20 +
    1.21  * The rule expand_if is now part of the default simpset. This means that
    1.22    the simplifier will eliminate all ocurrences of if-then-else in the
    1.23    conclusion of a goal. To prevent this, you can either remove expand_if
    1.24 @@ -31,9 +34,10 @@
    1.25    simpset: every datatype generates a suitable rule `split_t_case' (where t
    1.26    is the name of the datatype).
    1.27  
    1.28 -* New theory Vimage (inverse image of a function, syntax f-``B)
    1.29 +* new theory Vimage (inverse image of a function, syntax f-``B);
    1.30  
    1.31 -* Many new identities for unions, intersections, etc.
    1.32 +* many new identities for unions, intersections, etc.;
    1.33 +
    1.34  
    1.35  
    1.36  New in Isabelle98 (January 1998)
     2.1 --- a/src/HOL/Arith.thy	Mon Mar 09 16:17:28 1998 +0100
     2.2 +++ b/src/HOL/Arith.thy	Mon Mar 09 16:30:55 1998 +0100
     2.3 @@ -22,9 +22,6 @@
     2.4    diff_0   "m - 0 = m"
     2.5    diff_Suc "m - Suc n = (case m - n of 0 => 0 | Suc k => k)"
     2.6  
     2.7 -syntax pred :: nat => nat
     2.8 -translations "pred m" => "m - 1"
     2.9 -
    2.10  primrec "op *"  nat 
    2.11    mult_0   "0 * n = 0"
    2.12    mult_Suc "Suc m * n = n + (m * n)"