author | blanchet |
Tue, 13 Apr 2010 15:30:15 +0200 | |
changeset 36131 | 64b6374a21a8 |
parent 36130 | 9a672f7d488d |
child 36132 | 6afa012a8f5c |
--- 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 (*****************************************************************************)