--- a/src/HOL/Hoare/Pointers0.thy Mon Mar 01 16:42:45 2010 +0100
+++ b/src/HOL/Hoare/Pointers0.thy Mon Mar 01 17:05:57 2010 +0100
@@ -320,13 +320,11 @@
text"This is still a bit rough, especially the proof."
-consts merge :: "'a list * 'a list * ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list"
-
-recdef merge "measure(%(xs,ys,f). size xs + size ys)"
+fun merge :: "'a list * 'a list * ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list" where
"merge(x#xs,y#ys,f) = (if f x y then x # merge(xs,y#ys,f)
- else y # merge(x#xs,ys,f))"
-"merge(x#xs,[],f) = x # merge(xs,[],f)"
-"merge([],y#ys,f) = y # merge([],ys,f)"
+ else y # merge(x#xs,ys,f))" |
+"merge(x#xs,[],f) = x # merge(xs,[],f)" |
+"merge([],y#ys,f) = y # merge([],ys,f)" |
"merge([],[],f) = []"
lemma imp_disjCL: "(P|Q \<longrightarrow> R) = ((P \<longrightarrow> R) \<and> (~P \<longrightarrow> Q \<longrightarrow> R))"