# HG changeset patch
# User wenzelm
# Date 1159479767 -7200
# Node ID 7a51ed817ec79a108ff282e29a5c43326dcd049f
# Parent  89bec28a03c861b89512935df45d8b5c20091a28
tuned definitions/proofs;

diff -r 89bec28a03c8 -r 7a51ed817ec7 src/HOL/Real/RealVector.thy
--- 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)"
 by (simp add: of_real_def scaleR_cancel_right)
@@ -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