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]:
```