src/HOL/Basic_BNFs.thy
changeset 58446 e89f57d1e46c
parent 56077 d397030fb27e
child 58889 5b7a9633cfa8
     1.1 --- a/src/HOL/Basic_BNFs.thy	Thu Sep 25 16:35:51 2014 +0200
     1.2 +++ b/src/HOL/Basic_BNFs.thy	Thu Sep 25 16:35:53 2014 +0200
     1.3 @@ -21,14 +21,6 @@
     1.4  
     1.5  lemmas sum_set_defs = setl_def[abs_def] setr_def[abs_def]
     1.6  
     1.7 -definition
     1.8 -   rel_sum :: "('a \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> 'a + 'b \<Rightarrow> 'c + 'd \<Rightarrow> bool"
     1.9 -where
    1.10 -   "rel_sum R1 R2 x y =
    1.11 -     (case (x, y) of (Inl x, Inl y) \<Rightarrow> R1 x y
    1.12 -     | (Inr x, Inr y) \<Rightarrow> R2 x y
    1.13 -     | _ \<Rightarrow> False)"
    1.14 -
    1.15  lemma rel_sum_simps[simp]:
    1.16    "rel_sum R1 R2 (Inl a1) (Inl b1) = R1 a1 b1"
    1.17    "rel_sum R1 R2 (Inl a1) (Inr b2) = False"