src/HOL/ex/FinFunPred.thy

--- a/src/HOL/ex/FinFunPred.thy	Fri Jun 01 13:52:51 2012 +0200
+++ b/src/HOL/ex/FinFunPred.thy	Fri Jun 01 14:34:46 2012 +0200
@@ -258,4 +258,11 @@
   by eval
 end
 
+declare iso_finfun_Ball_Ball[code_unfold]
+notepad begin
+have "(\<forall>x. ((\<lambda>_ :: nat. False)(1 := True, 2 := True)) x \<longrightarrow> x < 3)"
+  by eval
+end
+declare iso_finfun_Ball_Ball[code_unfold del]
+
 end
\ No newline at end of file