# HG changeset patch
# User huffman
# Date 1321511497 -3600
# Node ID 7f5050fb88219c9741215e3269b72beb23b37a29
# Parent  787a1a097465391ad2ed4886e723df3c7548ba4f
name simp theorems st_0 and st_1

diff -r 787a1a097465 -r 7f5050fb8821 src/HOL/NSA/NSA.thy
--- a/src/HOL/NSA/NSA.thy	Thu Nov 17 07:15:30 2011 +0100
+++ b/src/HOL/NSA/NSA.thy	Thu Nov 17 07:31:37 2011 +0100
@@ -1874,9 +1874,11 @@
 lemma st_number_of [simp]: "st (number_of w) = number_of w"
 by (rule Reals_number_of [THEN st_SReal_eq])
 
-(*the theorem above for the special cases of zero and one*)
-lemma [simp]: "st 0 = 0" "st 1 = 1"
-by (simp_all add: st_SReal_eq)
+lemma st_0 [simp]: "st 0 = 0"
+by (simp add: st_SReal_eq)
+
+lemma st_1 [simp]: "st 1 = 1"
+by (simp add: st_SReal_eq)
 
 lemma st_minus: "x \<in> HFinite \<Longrightarrow> st (- x) = - st x"
 by (simp add: st_unique st_SReal st_approx_self approx_minus)
@@ -1934,14 +1936,12 @@
 done
 
 lemma st_zero_le: "[| 0 \<le> x;  x \<in> HFinite |] ==> 0 \<le> st x"
-apply (subst numeral_0_eq_0 [symmetric])
-apply (rule st_number_of [THEN subst])
+apply (subst st_0 [symmetric])
 apply (rule st_le, auto)
 done
 
 lemma st_zero_ge: "[| x \<le> 0;  x \<in> HFinite |] ==> st x \<le> 0"
-apply (subst numeral_0_eq_0 [symmetric])
-apply (rule st_number_of [THEN subst])
+apply (subst st_0 [symmetric])
 apply (rule st_le, auto)
 done