diff -r dd58f13a8eb4 -r eb85850d3eb7 src/HOL/Library/ExecutableRat.thy
--- a/src/HOL/Library/ExecutableRat.thy	Fri Nov 17 02:19:55 2006 +0100
+++ b/src/HOL/Library/ExecutableRat.thy	Fri Nov 17 02:20:03 2006 +0100
@@ -27,8 +27,8 @@
 instance erat :: ord ..
 
 definition
-  norm :: "erat \<Rightarrow> erat"
-  norm_def: "norm r = (case r of (Rat a p q) \<Rightarrow>
+  norm :: "erat \<Rightarrow> erat" where
+  "norm r = (case r of (Rat a p q) \<Rightarrow>
      if p = 0 then Rat True 0 1
      else
        let
@@ -36,19 +36,28 @@
        in let
          m = zgcd (absp, q)
        in Rat (a = (0 <= p)) (absp div m) (q div m))"
-  common :: "(int * int) * (int * int) \<Rightarrow> (int * int) * int"
-  common_def: "common r = (case r of ((p1, q1), (p2, q2)) \<Rightarrow>
+
+definition
+  common :: "(int * int) * (int * int) \<Rightarrow> (int * int) * int" where
+  "common r = (case r of ((p1, q1), (p2, q2)) \<Rightarrow>
        let q' = q1 * q2 div int (gcd (nat q1, nat q2))
        in ((p1 * (q' div q1), p2 * (q' div q2)), q'))"
-  of_quotient :: "int \<Rightarrow> int \<Rightarrow> erat"
-  of_quotient_def: "of_quotient a b =
-       norm (Rat True a b)"
-  of_rat :: "rat \<Rightarrow> erat"
-  of_rat_def: "of_rat r = split of_quotient (SOME s. s : Rep_Rat r)"
-  to_rat :: "erat \<Rightarrow> rat"
-  to_rat_def: "to_rat r = (case r of (Rat a p q) \<Rightarrow>
+
+definition
+  of_quotient :: "int \<Rightarrow> int \<Rightarrow> erat" where
+  "of_quotient a b = norm (Rat True a b)"
+
+definition
+  of_rat :: "rat \<Rightarrow> erat" where
+  "of_rat r = split of_quotient (SOME s. s : Rep_Rat r)"
+
+definition
+  to_rat :: "erat \<Rightarrow> rat" where
+  "to_rat r = (case r of (Rat a p q) \<Rightarrow>
        if a then Fract p q else Fract (uminus p) q)"
-  eq_erat :: "erat \<Rightarrow> erat \<Rightarrow> bool"
+
+definition
+  eq_erat :: "erat \<Rightarrow> erat \<Rightarrow> bool" where
   "eq_erat r s = (norm r = norm s)"
 
 axiomatization