src/HOL/Predicate.thy
changeset 38651 8aadda8e1338
parent 37767 a2b7a20d6ea3
child 38857 97775f3e8722
equal deleted inserted replaced
38650:f22a564ac820 38651:8aadda8e1338
    90   by (simp add: top_fun_eq top_bool_eq)
    90   by (simp add: top_fun_eq top_bool_eq)
    91 
    91 
    92 lemma top2I [intro!]: "top x y"
    92 lemma top2I [intro!]: "top x y"
    93   by (simp add: top_fun_eq top_bool_eq)
    93   by (simp add: top_fun_eq top_bool_eq)
    94 
    94 
    95 lemma bot1E [elim!]: "bot x \<Longrightarrow> P"
    95 lemma bot1E [no_atp, elim!]: "bot x \<Longrightarrow> P"
    96   by (simp add: bot_fun_eq bot_bool_eq)
    96   by (simp add: bot_fun_eq bot_bool_eq)
    97 
    97 
    98 lemma bot2E [elim!]: "bot x y \<Longrightarrow> P"
    98 lemma bot2E [elim!]: "bot x y \<Longrightarrow> P"
    99   by (simp add: bot_fun_eq bot_bool_eq)
    99   by (simp add: bot_fun_eq bot_bool_eq)
   100 
   100