author | traytel |
Tue, 16 Feb 2016 22:28:19 +0100 | |
changeset 62325 | 7e4d31eefe60 |
parent 62324 | ae44f16dcea5 |
child 62326 | 3cf7a067599c |
--- a/src/HOL/BNF_Fixpoint_Base.thy Tue Feb 16 22:28:19 2016 +0100 +++ b/src/HOL/BNF_Fixpoint_Base.thy Tue Feb 16 22:28:19 2016 +0100 @@ -73,12 +73,12 @@ "case_sum f g (if p then Inl x else Inr y) = (if p then f x else g y)" by simp -lemma prod_set_simps: +lemma prod_set_simps[simp]: "fsts (x, y) = {x}" "snds (x, y) = {y}" unfolding prod_set_defs by simp+ -lemma sum_set_simps: +lemma sum_set_simps[simp]: "setl (Inl x) = {x}" "setl (Inr x) = {}" "setr (Inl x) = {}"