lib: consistent naming in None_Top_Bot

none_bot_top_neq_None should indicated that it is about bool only, like the none_top_bot version. Signed-off-by: Gerwin Klein <[email protected]>
seL4 · Mar 16, 2024 · f3b6fbf · f3b6fbf
1 parent 36c4a43
commit f3b6fbf
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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 \<noteq> None)"
   by (cases opt) auto