proper definition of add_zero_left/right;
authorwenzelm
Wed Nov 08 13:48:34 2006 +0100 (2006-11-08)
changeset 2124523e6eb4d0975
parent 21244 0e9d222db727
child 21246 e0e555b67fe5
proper definition of add_zero_left/right;
src/HOL/OrderedGroup.thy
     1.1 --- a/src/HOL/OrderedGroup.thy	Wed Nov 08 13:48:33 2006 +0100
     1.2 +++ b/src/HOL/OrderedGroup.thy	Wed Nov 08 13:48:34 2006 +0100
     1.3 @@ -101,6 +101,9 @@
     1.4    finally show ?thesis .
     1.5  qed
     1.6  
     1.7 +lemmas add_zero_left = add_0
     1.8 +  and add_zero_right = add_0_right
     1.9 +
    1.10  lemma add_left_cancel [simp]:
    1.11       "(a + b = a + c) = (b = (c::'a::cancel_semigroup_add))"
    1.12  by (blast dest: add_left_imp_eq) 
    1.13 @@ -1055,13 +1058,6 @@
    1.14  declare diff_le_0_iff_le [simp]
    1.15  
    1.16  
    1.17 -
    1.18 -
    1.19 -ML {*
    1.20 -val add_zero_left = thm"add_0";
    1.21 -val add_zero_right = thm"add_0_right";
    1.22 -*}
    1.23 -
    1.24  ML {*
    1.25  val add_assoc = thm "add_assoc";
    1.26  val add_commute = thm "add_commute";