--- a/thys/Rec_Def.thy	Mon Feb 11 00:08:54 2013 +0000
+++ b/thys/Rec_Def.thy	Mon Feb 11 08:31:48 2013 +0000
@@ -2,42 +2,26 @@
 imports Main
 begin
 
-section {*
-  Recursive functions
-*}
-
-text {*
-  Datatype of recursive operators.
-*}
+section {* Recursive functions *}
 
 datatype recf = 
- -- {* The zero function, which always resturns @{text "0"} as result. *}
-  z | 
- -- {* The successor function, which increments its arguments. *}
-  s | 
- -- {*
-  The projection function, where @{text "id i j"} returns the @{text "j"}-th
-  argment out of the @{text "i"} arguments.
-  *}
+  z | s | 
+  -- {* The projection function, where @{text "id i j"} returns the @{text "j"}-th
+  argment out of the @{text "i"} arguments. *}
   id nat nat | 
- -- {*
-  The compostion operator, where "@{text "Cn n f [g1; g2; \<dots> ;gm]"} 
+  -- {* The compostion operator, where "@{text "Cn n f [g1; g2; \<dots> ;gm]"} 
   computes @{text "f (g1(x1, x2, \<dots>, xn), g2(x1, x2, \<dots>, xn), \<dots> , 
-  gm(x1, x2, \<dots> , xn))"} for input argments @{text "x1, \<dots>, xn"}.
-  *}
+  gm(x1, x2, \<dots> , xn))"} for input argments @{text "x1, \<dots>, xn"}. *}
   Cn nat recf "recf list" | 
--- {*
-  The primitive resursive operator, where @{text "Pr n f g"} computes:
+  -- {* The primitive resursive operator, where @{text "Pr n f g"} computes:
   @{text "Pr n f g (x1, x2, \<dots>, xn-1, 0) = f(x1, \<dots>, xn-1)"} 
   and @{text "Pr n f g (x1, x2, \<dots>, xn-1, k') = g(x1, x2, \<dots>, xn-1, k, 
-                                                  Pr n f g (x1, \<dots>, xn-1, k))"}.
+                                            Pr n f g (x1, \<dots>, xn-1, k))"}.
   *}
   Pr nat recf recf | 
--- {*
-  The minimization operator, where @{text "Mn n f (x1, x2, \<dots> , xn)"} 
+  -- {* The minimization operator, where @{text "Mn n f (x1, x2, \<dots> , xn)"} 
   computes the first i such that @{text "f (x1, \<dots>, xn, i) = 0"} and for all
-  @{text "j"}, @{text "f (x1, x2, \<dots>, xn, j) > 0"}.
-  *}
+  @{text "j"}, @{text "f (x1, x2, \<dots>, xn, j) > 0"}. *}
   Mn nat recf 
 
 text {* 
@@ -72,8 +56,7 @@
              \<forall> i < r. (\<exists> ri. rec_calc_rel f (args@[i]) ri \<and> ri \<noteq> 0)\<rbrakk> 
             \<Longrightarrow> rec_calc_rel (Mn n f) args r" 
 
-inductive_cases calc_pr_reverse:
-              "rec_calc_rel (Pr n f g) (lm) rSucy"
+inductive_cases calc_pr_reverse: "rec_calc_rel (Pr n f g) (lm) rSucy"
 
 inductive_cases calc_z_reverse: "rec_calc_rel z lm x"