slightly tuned

--- a/src/HOL/Code_Eval.thy	Wed Oct 22 14:15:42 2008 +0200
+++ b/src/HOL/Code_Eval.thy	Wed Oct 22 14:15:43 2008 +0200
@@ -15,14 +15,10 @@
 
 datatype "term" = dummy_term
 
-definition
-  Const :: "message_string \<Rightarrow> typerep \<Rightarrow> term"
-where
+definition Const :: "message_string \<Rightarrow> typerep \<Rightarrow> term" where
   "Const _ _ = dummy_term"
 
-definition
-  App :: "term \<Rightarrow> term \<Rightarrow> term"
-where
+definition App :: "term \<Rightarrow> term \<Rightarrow> term" where
   "App _ _ = dummy_term"
 
 code_datatype Const App

--- a/src/HOL/Int.thy	Wed Oct 22 14:15:42 2008 +0200
+++ b/src/HOL/Int.thy	Wed Oct 22 14:15:43 2008 +0200
@@ -21,9 +21,7 @@
 
 subsection {* The equivalence relation underlying the integers *}
 
-definition
-  intrel :: "((nat \<times> nat) \<times> (nat \<times> nat)) set"
-where
+definition intrel :: "((nat \<times> nat) \<times> (nat \<times> nat)) set" where
   [code del]: "intrel = {((x, y), (u, v)) | x y u v. x + v = u +y }"
 
 typedef (Integ)

--- a/src/HOL/ex/Efficient_Nat_examples.thy	Wed Oct 22 14:15:42 2008 +0200
+++ b/src/HOL/ex/Efficient_Nat_examples.thy	Wed Oct 22 14:15:43 2008 +0200
@@ -9,34 +9,24 @@
 imports Main "~~/src/HOL/Real/RealDef" Efficient_Nat
 begin
 
-fun
-  to_n :: "nat \<Rightarrow> nat list"
-where
+fun to_n :: "nat \<Rightarrow> nat list" where
   "to_n 0 = []"
   | "to_n (Suc 0) = []"
   | "to_n (Suc (Suc 0)) = []"
   | "to_n (Suc n) = n # to_n n"
 
-definition
-  naive_prime :: "nat \<Rightarrow> bool"
-where
+definition naive_prime :: "nat \<Rightarrow> bool" where
   "naive_prime n \<longleftrightarrow> n \<ge> 2 \<and> filter (\<lambda>m. n mod m = 0) (to_n n) = []"
 
-primrec
-  fac :: "nat \<Rightarrow> nat"
-where
+primrec fac :: "nat \<Rightarrow> nat" where
   "fac 0 = 1"
   | "fac (Suc n) = Suc n * fac n"
 
-primrec
-  rat_of_nat :: "nat \<Rightarrow> rat"
-where
+primrec rat_of_nat :: "nat \<Rightarrow> rat" where
   "rat_of_nat 0 = 0"
   | "rat_of_nat (Suc n) = rat_of_nat n + 1"
 
-primrec
-  harmonic :: "nat \<Rightarrow> rat"
-where
+primrec harmonic :: "nat \<Rightarrow> rat" where
   "harmonic 0 = 0"
   | "harmonic (Suc n) = 1 / rat_of_nat (Suc n) + harmonic n"