# HG changeset patch
# User traytel
# Date 1455658099 -3600
# Node ID 7e4d31eefe6084f9db387d2bd16c1f6741957860
# Parent  ae44f16dcea513c3e33d1bbf5369b452b77c6a1e
simp rules for fsts, snds, setl, setr

diff -r ae44f16dcea5 -r 7e4d31eefe60 src/HOL/BNF_Fixpoint_Base.thy
--- 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) = {}"