src/HOL/Induct/Tree.thy

--- a/src/HOL/Induct/Tree.thy	Tue Mar 13 23:45:34 2012 +0100
+++ b/src/HOL/Induct/Tree.thy	Wed Mar 14 00:34:56 2012 +0100
@@ -13,8 +13,7 @@
     Atom 'a
   | Branch "nat => 'a tree"
 
-primrec
-  map_tree :: "('a => 'b) => 'a tree => 'b tree"
+primrec map_tree :: "('a => 'b) => 'a tree => 'b tree"
 where
   "map_tree f (Atom a) = Atom (f a)"
 | "map_tree f (Branch ts) = Branch (\<lambda>x. map_tree f (ts x))"
@@ -22,8 +21,7 @@
 lemma tree_map_compose: "map_tree g (map_tree f t) = map_tree (g \<circ> f) t"
   by (induct t) simp_all
 
-primrec
-  exists_tree :: "('a => bool) => 'a tree => bool"
+primrec exists_tree :: "('a => bool) => 'a tree => bool"
 where
   "exists_tree P (Atom a) = P a"
 | "exists_tree P (Branch ts) = (\<exists>x. exists_tree P (ts x))"
@@ -39,8 +37,7 @@
 datatype brouwer = Zero | Succ "brouwer" | Lim "nat => brouwer"
 
 text{*Addition of ordinals*}
-primrec
-  add :: "[brouwer,brouwer] => brouwer"
+primrec add :: "[brouwer,brouwer] => brouwer"
 where
   "add i Zero = i"
 | "add i (Succ j) = Succ (add i j)"
@@ -50,8 +47,7 @@
   by (induct k) auto
 
 text{*Multiplication of ordinals*}
-primrec
-  mult :: "[brouwer,brouwer] => brouwer"
+primrec mult :: "[brouwer,brouwer] => brouwer"
 where
   "mult i Zero = Zero"
 | "mult i (Succ j) = add (mult i j) i"
@@ -72,13 +68,11 @@
   ordinals.  Start with a predecessor relation and form its transitive 
   closure. *} 
 
-definition
-  brouwer_pred :: "(brouwer * brouwer) set" where
-  "brouwer_pred = (\<Union>i. {(m,n). n = Succ m \<or> (EX f. n = Lim f & m = f i)})"
+definition brouwer_pred :: "(brouwer * brouwer) set"
+  where "brouwer_pred = (\<Union>i. {(m,n). n = Succ m \<or> (EX f. n = Lim f & m = f i)})"
 
-definition
-  brouwer_order :: "(brouwer * brouwer) set" where
-  "brouwer_order = brouwer_pred^+"
+definition brouwer_order :: "(brouwer * brouwer) set"
+  where "brouwer_order = brouwer_pred^+"
 
 lemma wf_brouwer_pred: "wf brouwer_pred"
   by(unfold wf_def brouwer_pred_def, clarify, induct_tac x, blast+)
@@ -94,8 +88,7 @@
 
 text{*Example of a general function*}
 
-function
-  add2 :: "brouwer \<Rightarrow> brouwer \<Rightarrow> brouwer"
+function add2 :: "brouwer \<Rightarrow> brouwer \<Rightarrow> brouwer"
 where
   "add2 i Zero = i"
 | "add2 i (Succ j) = Succ (add2 i j)"