src/HOL/Hyperreal/NSA.thy
changeset 23096 423ad2fe9f76
parent 23078 e5670ceef56f
child 25062 af5ef0d4d655
     1.1 --- a/src/HOL/Hyperreal/NSA.thy	Thu May 24 16:52:54 2007 +0200
     1.2 +++ b/src/HOL/Hyperreal/NSA.thy	Thu May 24 22:55:53 2007 +0200
     1.3 @@ -1723,13 +1723,13 @@
     1.4       "(x::hypreal)*x + y*y \<in> Infinitesimal ==> x*x \<in> Infinitesimal"
     1.5  apply (rule Infinitesimal_interval2)
     1.6  apply (rule_tac [3] zero_le_square, assumption)
     1.7 -apply (auto simp add: zero_le_square)
     1.8 +apply (auto)
     1.9  done
    1.10  
    1.11  lemma HFinite_square_cancel [simp]:
    1.12    "(x::hypreal)*x + y*y \<in> HFinite ==> x*x \<in> HFinite"
    1.13  apply (rule HFinite_bounded, assumption)
    1.14 -apply (auto simp add: zero_le_square)
    1.15 +apply (auto)
    1.16  done
    1.17  
    1.18  lemma Infinitesimal_square_cancel2 [simp]:
    1.19 @@ -1751,7 +1751,7 @@
    1.20  apply (rule Infinitesimal_interval2, assumption)
    1.21  apply (rule_tac [2] zero_le_square, simp)
    1.22  apply (insert zero_le_square [of y]) 
    1.23 -apply (insert zero_le_square [of z], simp)
    1.24 +apply (insert zero_le_square [of z], simp del:zero_le_square)
    1.25  done
    1.26  
    1.27  lemma HFinite_sum_square_cancel [simp]:
    1.28 @@ -1759,7 +1759,7 @@
    1.29  apply (rule HFinite_bounded, assumption)
    1.30  apply (rule_tac [2] zero_le_square)
    1.31  apply (insert zero_le_square [of y]) 
    1.32 -apply (insert zero_le_square [of z], simp)
    1.33 +apply (insert zero_le_square [of z], simp del:zero_le_square)
    1.34  done
    1.35  
    1.36  lemma Infinitesimal_sum_square_cancel2 [simp]: