1.1 --- a/src/HOL/Word/BinOperations.thy	Thu Aug 28 15:33:33 2008 +0200
     1.2 +++ b/src/HOL/Word/BinOperations.thy	Thu Aug 28 17:54:18 2008 +0200
     1.3 @@ -514,24 +514,20 @@
     1.4  definition bin_rcat :: "nat \<Rightarrow> int list \<Rightarrow> int" where
     1.5    "bin_rcat n = foldl (%u v. bin_cat u n v) Int.Pls"
     1.6  
     1.7 -function bin_rsplit_aux :: "nat \<Rightarrow> nat \<Rightarrow> int \<Rightarrow> int list \<Rightarrow> int list" where
     1.8 +fun bin_rsplit_aux :: "nat \<Rightarrow> nat \<Rightarrow> int \<Rightarrow> int list \<Rightarrow> int list" where
     1.9    "bin_rsplit_aux n m c bs =
    1.10      (if m = 0 | n = 0 then bs else
    1.11        let (a, b) = bin_split n c 
    1.12        in bin_rsplit_aux n (m - n) a (b # bs))"
    1.13 -by pat_completeness auto
    1.14 -termination by (relation "measure (fst o snd)") simp_all
    1.15  
    1.16  definition bin_rsplit :: "nat \<Rightarrow> nat \<times> int \<Rightarrow> int list" where
    1.17    "bin_rsplit n w = bin_rsplit_aux n (fst w) (snd w) []"
    1.18  
    1.19 -function bin_rsplitl_aux :: "nat \<Rightarrow> nat \<Rightarrow> int \<Rightarrow> int list \<Rightarrow> int list" where
    1.20 +fun bin_rsplitl_aux :: "nat \<Rightarrow> nat \<Rightarrow> int \<Rightarrow> int list \<Rightarrow> int list" where
    1.21    "bin_rsplitl_aux n m c bs =
    1.22      (if m = 0 | n = 0 then bs else
    1.23        let (a, b) = bin_split (min m n) c 
    1.24        in bin_rsplitl_aux n (m - n) a (b # bs))"
    1.25 -by pat_completeness auto
    1.26 -termination by (relation "measure (fst o snd)") simp_all
    1.27  
    1.28  definition bin_rsplitl :: "nat \<Rightarrow> nat \<times> int \<Rightarrow> int list" where
    1.29    "bin_rsplitl n w = bin_rsplitl_aux n (fst w) (snd w) []"