diff --git a/lib/None_Top_Bot.thy b/lib/None_Top_Bot.thy index e331e06bfe..6f9faf7c16 100644 --- a/lib/None_Top_Bot.thy +++ b/lib/None_Top_Bot.thy @@ -184,7 +184,7 @@ lemma none_bot_boolE: (* As for none_top_bot, it would be unusual to see "top" for bool. Only adding the lemma here for completeness *) -lemma none_bot_top_neq_None[simp]: +lemma none_bot_top_bool_neq_None[simp]: "none_bot top opt = (opt \ None)" by (cases opt) auto