src/HOL/Import/HOL4Compat.thy
changeset 15003 6145dd7538d7
parent 14620 1be590fd2422
child 16417 9bc16273c2d4
     1.1 --- a/src/HOL/Import/HOL4Compat.thy	Thu Jun 24 17:51:28 2004 +0200
     1.2 +++ b/src/HOL/Import/HOL4Compat.thy	Thu Jun 24 17:52:02 2004 +0200
     1.3 @@ -510,10 +510,10 @@
     1.4    by (simp add: real_of_nat_Suc)
     1.5  
     1.6  lemma abs: "abs (x::real) = (if 0 <= x then x else -x)"
     1.7 -  by (simp add: real_abs_def)
     1.8 +  by (simp add: abs_if)
     1.9  
    1.10  lemma pow: "(!x::real. x ^ 0 = 1) & (!x::real. ALL n. x ^ (Suc n) = x * x ^ n)"
    1.11 -  by simp;
    1.12 +  by simp
    1.13  
    1.14  constdefs
    1.15    real_gt :: "real => real => bool"