| changeset 36131 | 64b6374a21a8 |
| parent 35416 | d8d7d1b785af |
| child 36319 | 8feb2c4bef1a |
--- 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 (*****************************************************************************)