diff -r dd58f13a8eb4 -r eb85850d3eb7 src/HOL/ex/Classpackage.thy
--- a/src/HOL/ex/Classpackage.thy	Fri Nov 17 02:19:55 2006 +0100
+++ b/src/HOL/ex/Classpackage.thy	Fri Nov 17 02:20:03 2006 +0100
@@ -97,8 +97,8 @@
 qed
 
 definition (in monoid)
-  units :: "'a set"
-  units_def: "units = { y. \<exists>x. x \<^loc>\<otimes> y = \<^loc>\<one> \<and> y \<^loc>\<otimes> x = \<^loc>\<one> }"
+  units :: "'a set" where
+  "units = { y. \<exists>x. x \<^loc>\<otimes> y = \<^loc>\<one> \<and> y \<^loc>\<otimes> x = \<^loc>\<one> }"
 
 lemma (in monoid) inv_obtain:
   assumes ass: "x \<in> units"
@@ -139,11 +139,11 @@
   "reduce f g (Suc n) x = f x (reduce f g n x)"
 
 definition (in monoid)
-  npow :: "nat \<Rightarrow> 'a \<Rightarrow> 'a"
+  npow :: "nat \<Rightarrow> 'a \<Rightarrow> 'a" where
   npow_def_prim: "npow n x = reduce (op \<^loc>\<otimes>) \<^loc>\<one> n x"
 
 abbreviation (in monoid)
-  abbrev_npow :: "'a \<Rightarrow> nat \<Rightarrow> 'a" (infix "\<^loc>\<up>" 75)
+  abbrev_npow :: "'a \<Rightarrow> nat \<Rightarrow> 'a" (infix "\<^loc>\<up>" 75) where
   "x \<^loc>\<up> n \<equiv> npow n x"
 
 lemma (in monoid) npow_def:
@@ -272,12 +272,12 @@
 using invr invl by simp
 
 definition (in group)
-  pow :: "int \<Rightarrow> 'a \<Rightarrow> 'a"
-  pow_def: "pow k x = (if k < 0 then \<^loc>\<div> (monoid.npow (op \<^loc>\<otimes>) \<^loc>\<one> (nat (-k)) x)
+  pow :: "int \<Rightarrow> 'a \<Rightarrow> 'a" where
+  "pow k x = (if k < 0 then \<^loc>\<div> (monoid.npow (op \<^loc>\<otimes>) \<^loc>\<one> (nat (-k)) x)
     else (monoid.npow (op \<^loc>\<otimes>) \<^loc>\<one> (nat k) x))"
 
 abbreviation (in group)
-  abbrev_pow :: "'a \<Rightarrow> int \<Rightarrow> 'a" (infix "\<^loc>\<up>" 75)
+  abbrev_pow :: "'a \<Rightarrow> int \<Rightarrow> 'a" (infix "\<^loc>\<up>" 75) where
   "x \<^loc>\<up> k \<equiv> pow k x"
 
 lemma (in group) int_pow_zero:
@@ -312,12 +312,12 @@
 
 definition
   "X a b c = (a \<otimes> \<one> \<otimes> b, a \<otimes> \<one> \<otimes> b, [a, b] \<otimes> \<one> \<otimes> [a, b, c])"
+definition
   "Y a b c = (a, \<div> a) \<otimes> \<one> \<otimes> \<div> (b, \<div> c)"
 
-definition
-  "x1 = X (1::nat) 2 3"
-  "x2 = X (1::int) 2 3"
-  "y2 = Y (1::int) 2 3"
+definition "x1 = X (1::nat) 2 3"
+definition "x2 = X (1::int) 2 3"
+definition "y2 = Y (1::int) 2 3"
 
 code_gen "op \<otimes>" \<one> inv
 code_gen X Y (SML) (Haskell)