dropped obsolete FIXMEs
authorkrauss
Tue, 22 Feb 2011 16:47:18 +0100
changeset 41817 c7be23634728
parent 41816 7a55699805dc
child 41818 6d4c3ee8219d
dropped obsolete FIXMEs
src/HOL/ex/Fundefs.thy
--- 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))"