src/HOL/Hoare/Pointers0.thy
changeset 35419 d78659d1723e
parent 35416 d8d7d1b785af
child 38353 d98baa2cf589
     1.1 --- a/src/HOL/Hoare/Pointers0.thy	Mon Mar 01 16:42:45 2010 +0100
     1.2 +++ b/src/HOL/Hoare/Pointers0.thy	Mon Mar 01 17:05:57 2010 +0100
     1.3 @@ -320,13 +320,11 @@
     1.4  
     1.5  text"This is still a bit rough, especially the proof."
     1.6  
     1.7 -consts merge :: "'a list * 'a list * ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list"
     1.8 -
     1.9 -recdef merge "measure(%(xs,ys,f). size xs + size ys)"
    1.10 +fun merge :: "'a list * 'a list * ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list" where
    1.11  "merge(x#xs,y#ys,f) = (if f x y then x # merge(xs,y#ys,f)
    1.12 -                                else y # merge(x#xs,ys,f))"
    1.13 -"merge(x#xs,[],f) = x # merge(xs,[],f)"
    1.14 -"merge([],y#ys,f) = y # merge([],ys,f)"
    1.15 +                                else y # merge(x#xs,ys,f))" |
    1.16 +"merge(x#xs,[],f) = x # merge(xs,[],f)" |
    1.17 +"merge([],y#ys,f) = y # merge([],ys,f)" |
    1.18  "merge([],[],f) = []"
    1.19  
    1.20  lemma imp_disjCL: "(P|Q \<longrightarrow> R) = ((P \<longrightarrow> R) \<and> (~P \<longrightarrow> Q \<longrightarrow> R))"