src/HOL/Basic_BNFs.thy
changeset 55707 50cf04dd2584
parent 55084 8ee9aabb2bca
child 55811 aa1acc25126b
     1.1 --- a/src/HOL/Basic_BNFs.thy	Mon Feb 24 00:04:48 2014 +0100
     1.2 +++ b/src/HOL/Basic_BNFs.thy	Mon Feb 24 10:16:10 2014 +0100
     1.3 @@ -25,11 +25,9 @@
     1.4  
     1.5  bnf DEADID: 'a
     1.6    map: "id :: 'a \<Rightarrow> 'a"
     1.7 -  bd: "natLeq +c |UNIV :: 'a set|"
     1.8 +  bd: natLeq
     1.9    rel: "op = :: 'a \<Rightarrow> 'a \<Rightarrow> bool"
    1.10 -by (auto simp add: Grp_def
    1.11 -  card_order_csum natLeq_card_order card_of_card_order_on
    1.12 -  cinfinite_csum natLeq_cinfinite)
    1.13 +by (auto simp add: Grp_def natLeq_card_order natLeq_cinfinite)
    1.14  
    1.15  definition setl :: "'a + 'b \<Rightarrow> 'a set" where
    1.16  "setl x = (case x of Inl z => {z} | _ => {})"