# HG changeset patch
# User blanchet
# Date 1271165415 -7200
# Node ID 64b6374a21a81741bc571d9d2e65752c2e647332
# Parent  9a672f7d488dabd5ed0c75a97a97ebfc75ea7ec9
adapt Refute example to reflect latest soundness fix to Refute

diff -r 9a672f7d488d -r 64b6374a21a8 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
 
 (*****************************************************************************)