1.1 --- a/src/HOL/Lifting_Product.thy	Mon Jan 20 20:00:33 2014 +0100
     1.2 +++ b/src/HOL/Lifting_Product.thy	Mon Jan 20 20:21:12 2014 +0100
     1.3 @@ -5,23 +5,14 @@
     1.4  header {* Setup for Lifting/Transfer for the product type *}
     1.5  
     1.6  theory Lifting_Product
     1.7 -imports Lifting
     1.8 +imports Lifting Basic_BNFs
     1.9  begin
    1.10  
    1.11  subsection {* Relator and predicator properties *}
    1.12  
    1.13 -definition
    1.14 -  prod_rel :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('c \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> 'a \<times> 'c \<Rightarrow> 'b \<times> 'd \<Rightarrow> bool"
    1.15 -where
    1.16 -  "prod_rel R1 R2 = (\<lambda>(a, b) (c, d). R1 a c \<and> R2 b d)"
    1.17 -
    1.18  definition prod_pred :: "('a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
    1.19  where "prod_pred R1 R2 = (\<lambda>(a, b). R1 a \<and> R2 b)"
    1.20  
    1.21 -lemma prod_rel_apply [simp]:
    1.22 -  "prod_rel R1 R2 (a, b) (c, d) \<longleftrightarrow> R1 a c \<and> R2 b d"
    1.23 -  by (simp add: prod_rel_def)
    1.24 -
    1.25  lemma prod_pred_apply [simp]:
    1.26    "prod_pred P1 P2 (a, b) \<longleftrightarrow> P1 a \<and> P2 b"
    1.27    by (simp add: prod_pred_def)