| changeset 33199 | 6c9b2a94a69c |
| parent 33197 | de6285ebcc05 |
| child 34082 | 61b7aa37f4b7 |
--- a/src/HOL/Nitpick_Examples/Core_Nits.thy Fri Oct 23 19:00:36 2009 +0200 +++ b/src/HOL/Nitpick_Examples/Core_Nits.thy Fri Oct 23 20:13:33 2009 +0200 @@ -714,7 +714,7 @@ lemma "{} = (\<lambda>x. False)" nitpick [expect = none] -by (metis Collect_def bot_set_eq empty_def) +by (metis Collect_def empty_def) lemma "x \<in> {}" nitpick [expect = genuine]