equal
deleted
inserted
replaced
20 -- "prefer plain propositional version" |
20 -- "prefer plain propositional version" |
21 |
21 |
22 lemma |
22 lemma |
23 shows [code]: "HOL.equal False P \<longleftrightarrow> \<not> P" |
23 shows [code]: "HOL.equal False P \<longleftrightarrow> \<not> P" |
24 and [code]: "HOL.equal True P \<longleftrightarrow> P" |
24 and [code]: "HOL.equal True P \<longleftrightarrow> P" |
25 and [code]: "HOL.equal P False \<longleftrightarrow> \<not> P" |
25 and [code]: "HOL.equal P False \<longleftrightarrow> \<not> P" |
26 and [code]: "HOL.equal P True \<longleftrightarrow> P" |
26 and [code]: "HOL.equal P True \<longleftrightarrow> P" |
27 and [code nbe]: "HOL.equal P P \<longleftrightarrow> True" |
27 and [code nbe]: "HOL.equal P P \<longleftrightarrow> True" |
28 by (simp_all add: equal) |
28 by (simp_all add: equal) |
29 |
29 |
30 lemma If_case_cert: |
30 lemma If_case_cert: |