src/HOL/ex/FinFunPred.thy

 have "inf ((\<lambda>_ :: nat. False)(1 := True, 2 := True)) ((\<lambda>_. True)(3 := False)) \<le> 
       sup ((\<lambda>_. False)(1 := True, 5 := True)) (- ((\<lambda>_. True)(2 := False, 3 := False)))"
   by eval
 end
 
-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