adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

word-lib: remove unused if/option lemma 

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This commit is contained in:
Gerwin Klein 2022-06-04 19:27:33 +10:00 committed by Gerwin Klein
parent 8c796c5240
commit a45d32e574
1 changed files with 0 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
lib/Word_Lib/Many_More.thy
View File

@ -441,10 +441,6 @@ lemma sum_map_simps[simp]:
"sum_map f g (Inr w) = Inr (g w)"
by (simp add: sum_map_def)+
lemma if_Some_None_eq_None:
"((if P then Some v else None) = None) = (\<not> P)"
by simp
lemma CollectPairFalse [iff]:
"{(a,b). False} = {}"
by (simp add: split_def)