author | krauss |
Tue, 22 Feb 2011 16:47:18 +0100 | |
changeset 41817 | c7be23634728 |
parent 41816 | 7a55699805dc |
child 41818 | 6d4c3ee8219d |
--- a/src/HOL/ex/Fundefs.thy Mon Feb 21 23:54:53 2011 +0100 +++ b/src/HOL/ex/Fundefs.thy Tue Feb 22 16:47:18 2011 +0100 @@ -280,14 +280,12 @@ (* There were some problems with fresh names\<dots> *) -(* FIXME: tailrec? *) function k :: "nat \<Rightarrow> nat" where "k x = (let a = x; b = x in k x)" by pat_completeness auto -(* FIXME: tailrec? *) function f2 :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat)" where "f2 p = (let (x,y) = p in f2 (y,x))"