adapt Refute example to reflect latest soundness fix to Refute
authorblanchet
Tue, 13 Apr 2010 15:30:15 +0200
changeset 36131 64b6374a21a8
parent 36130 9a672f7d488d
child 36132 6afa012a8f5c
adapt Refute example to reflect latest soundness fix to Refute
src/HOL/ex/Refute_Examples.thy
--- a/src/HOL/ex/Refute_Examples.thy	Tue Apr 13 15:16:54 2010 +0200
+++ b/src/HOL/ex/Refute_Examples.thy	Tue Apr 13 15:30:15 2010 +0200
@@ -1361,7 +1361,8 @@
 | "x : a_odd \<Longrightarrow> f x : a_even"
 
 lemma "x : a_odd"
-  refute  -- {* finds a model of size 2, as expected *}
+  (* refute  -- {* finds a model of size 2, as expected *}
+     NO LONGER WORKS since "lfp"'s interpreter is disabled *)
 oops
 
 (*****************************************************************************)