1.1 --- a/src/HOL/Lifting_Product.thy	Thu Apr 10 17:48:32 2014 +0200
     1.2 +++ b/src/HOL/Lifting_Product.thy	Thu Apr 10 17:48:33 2014 +0200
     1.3 @@ -8,6 +8,11 @@
     1.4  imports Lifting Basic_BNFs
     1.5  begin
     1.6  
     1.7 +(* The following lemma can be deleted when product is added to FP sugar *)
     1.8 +lemma prod_pred_inject [simp]:
     1.9 +  "pred_prod P1 P2 (a, b) = (P1 a \<and> P2 b)"
    1.10 +  unfolding pred_prod_def fun_eq_iff prod_set_simps by blast
    1.11 +
    1.12  subsection {* Transfer rules for the Transfer package *}
    1.13  
    1.14  context

     2.1 --- a/src/HOL/Lifting_Sum.thy	Thu Apr 10 17:48:32 2014 +0200
     2.2 +++ b/src/HOL/Lifting_Sum.thy	Thu Apr 10 17:48:33 2014 +0200
     2.3 @@ -8,6 +8,11 @@
     2.4  imports Lifting Basic_BNFs
     2.5  begin
     2.6  
     2.7 +(* The following lemma can be deleted when sum is added to FP sugar *)
     2.8 +lemma sum_pred_inject [simp]:
     2.9 +  "pred_sum P1 P2 (Inl a) = P1 a" and "pred_sum P1 P2 (Inr a) = P2 a"
    2.10 +  unfolding pred_sum_def fun_eq_iff sum_set_simps by auto
    2.11 +
    2.12  subsection {* Transfer rules for the Transfer package *}
    2.13  
    2.14  context