author wenzelm Thu, 28 Sep 2006 23:42:47 +0200 changeset 20772 7a51ed817ec7 parent 20771 89bec28a03c8 child 20773 468af396cf6f
tuned definitions/proofs;
```--- a/src/HOL/Real/RealVector.thy	Thu Sep 28 23:42:45 2006 +0200
+++ b/src/HOL/Real/RealVector.thy	Thu Sep 28 23:42:47 2006 +0200
@@ -221,7 +221,7 @@

lemma of_real_power [simp]:
"of_real (x ^ n) = (of_real x :: 'a::{real_algebra_1,recpower}) ^ n"
-by (induct n, simp_all add: power_Suc)
+by (induct n) (simp_all add: power_Suc)

lemma of_real_eq_iff [simp]: "(of_real x = of_real y) = (x = y)"
@@ -237,7 +237,7 @@

text{*Collapse nested embeddings*}
lemma of_real_of_nat_eq [simp]: "of_real (of_nat n) = of_nat n"
-by (induct n, auto)
+by (induct n) auto

lemma of_real_of_int_eq [simp]: "of_real (of_int z) = of_int z"
by (cases z rule: int_diff_cases, simp)
@@ -249,9 +249,9 @@

subsection {* The Set of Real Numbers *}

-constdefs
-   Reals :: "'a::real_algebra_1 set"
-   "Reals \<equiv> range of_real"
+definition
+  Reals :: "'a::real_algebra_1 set"
+  "Reals \<equiv> range of_real"

const_syntax (xsymbols)
Reals  ("\<real>")
@@ -514,6 +514,6 @@
lemma norm_power:
fixes x :: "'a::{real_normed_div_algebra,recpower}"
shows "norm (x ^ n) = norm x ^ n"
-by (induct n, simp, simp add: power_Suc norm_mult)
+by (induct n) (simp_all add: power_Suc norm_mult)

end```