# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1361900317 0
# Node ID fdfd921ad2e295e7df577b6bbe1e34c5a9ad3e5a
# Parent  d93cc4295306ee694ca70f6f14dc05051f61f117
tuned

diff -r d93cc4295306 -r fdfd921ad2e2 thys/UF.thy
--- a/thys/UF.thy	Tue Feb 26 13:24:40 2013 +0000
+++ b/thys/UF.thy	Tue Feb 26 17:38:37 2013 +0000
@@ -562,7 +562,7 @@
 done
 
 text {*
-  Defintiion of @{text "Min[R]"} on page 77 of Boolos's book.
+  Definition of @{text "Min[R]"} on page 77 of Boolos's book.
 *}
 
 fun Minr :: "(nat list \<Rightarrow> bool) \<Rightarrow> nat list \<Rightarrow> nat \<Rightarrow> nat"
@@ -848,7 +848,7 @@
 by(auto simp: rec_le_def rec_exec.simps)
 
 text {*
-  Defintiion of @{text "Max[Rr]"} on page 77 of Boolos's book.
+  Definition of @{text "Max[Rr]"} on page 77 of Boolos's book.
 *}
 
 fun Maxr :: "(nat list \<Rightarrow> bool) \<Rightarrow> nat list \<Rightarrow> nat \<Rightarrow> nat"
@@ -874,7 +874,6 @@
                             (vl - 1) @ 
                              [id (Suc (Suc vl)) ((Suc vl))])] in
                   let rf = Cn (Suc (Suc vl)) rec_disj [rf1, rf2] in
-                  let rq = rec_all rt rf  in
                   let Qf = Cn (Suc vl) rec_not [rec_all rt rf]
                   in Cn vl (rec_sigma Qf) (get_fstn_args vl vl @
                                                          [id vl (vl - 1)]))"
@@ -2176,8 +2175,7 @@
 fun rec_listsum2 :: "nat \<Rightarrow> nat \<Rightarrow> recf"
   where
   "rec_listsum2 vl 0 = Cn vl z [id vl 0]"
-| "rec_listsum2 vl (Suc n) = Cn vl rec_add 
-                      [rec_listsum2 vl n, id vl (n)]"
+| "rec_listsum2 vl (Suc n) = Cn vl rec_add [rec_listsum2 vl n, id vl n]"
 
 declare listsum2.simps[simp del] rec_listsum2.simps[simp del]
 
@@ -2223,7 +2221,7 @@
 
 fun rec_map :: "recf \<Rightarrow> nat \<Rightarrow> recf list"
   where
-  "rec_map rf vl = map (\<lambda> i. Cn vl rf [id vl (i)]) [0..<vl]"
+  "rec_map rf vl = map (\<lambda> i. Cn vl rf [id vl i]) [0..<vl]"
 
 text {*
   @{text "rec_strt"} is the recursive function used to implement @{text "strt"}.