src/HOL/Basic_BNFs.thy
changeset 55935 8f20d09d294e
parent 55932 68c5104d2204
child 55943 5c2df04e97d1
     1.1 --- a/src/HOL/Basic_BNFs.thy	Thu Mar 06 13:36:50 2014 +0100
     1.2 +++ b/src/HOL/Basic_BNFs.thy	Thu Mar 06 14:14:54 2014 +0100
     1.3 @@ -13,22 +13,6 @@
     1.4  imports BNF_Def
     1.5  begin
     1.6  
     1.7 -bnf ID: 'a
     1.8 -  map: "id :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
     1.9 -  sets: "\<lambda>x. {x}"
    1.10 -  bd: natLeq
    1.11 -  rel: "id :: ('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool"
    1.12 -apply (auto simp: Grp_def fun_eq_iff relcompp.simps natLeq_card_order natLeq_cinfinite)
    1.13 -apply (rule ordLess_imp_ordLeq[OF finite_ordLess_infinite[OF _ natLeq_Well_order]])
    1.14 -apply (auto simp add: Field_card_of Field_natLeq card_of_well_order_on)[3]
    1.15 -done
    1.16 -
    1.17 -bnf DEADID: 'a
    1.18 -  map: "id :: 'a \<Rightarrow> 'a"
    1.19 -  bd: natLeq
    1.20 -  rel: "op = :: 'a \<Rightarrow> 'a \<Rightarrow> bool"
    1.21 -by (auto simp add: Grp_def natLeq_card_order natLeq_cinfinite)
    1.22 -
    1.23  definition setl :: "'a + 'b \<Rightarrow> 'a set" where
    1.24  "setl x = (case x of Inl z => {z} | _ => {})"
    1.25