src/HOL/Codatatype/BNF_Util.thy
changeset 49283 97809ae5f7bb
parent 49282 c057e1b39f16
child 49309 f20b24214ac2
equal deleted inserted replaced
49282:c057e1b39f16 49283:97809ae5f7bb
    11 theory BNF_Util
    11 theory BNF_Util
    12 imports
    12 imports
    13   "../Ordinals_and_Cardinals/Cardinal_Arithmetic"
    13   "../Ordinals_and_Cardinals/Cardinal_Arithmetic"
    14   "~~/src/HOL/Library/Prefix_Order"
    14   "~~/src/HOL/Library/Prefix_Order"
    15   Equiv_Relations_More
    15   Equiv_Relations_More
       
    16 uses
       
    17   ("Tools/bnf_util.ML")
    16 begin
    18 begin
    17 
    19 
    18 lemma iffI_np: "\<lbrakk>x \<Longrightarrow> \<not> y; \<not> x \<Longrightarrow> y\<rbrakk> \<Longrightarrow> \<not> x \<longleftrightarrow> y"
    20 lemma iffI_np: "\<lbrakk>x \<Longrightarrow> \<not> y; \<not> x \<Longrightarrow> y\<rbrakk> \<Longrightarrow> \<not> x \<longleftrightarrow> y"
    19 by (erule iffI) (erule contrapos_pn)
    21 by (erule iffI) (erule contrapos_pn)
    20 
    22 
   849 by simp
   851 by simp
   850 
   852 
   851 lemma not_arg_cong_Inr: "x \<noteq> y \<Longrightarrow> Inr x \<noteq> Inr y"
   853 lemma not_arg_cong_Inr: "x \<noteq> y \<Longrightarrow> Inr x \<noteq> Inr y"
   852 by simp
   854 by simp
   853 
   855 
       
   856 ML_file "Tools/bnf_util.ML"
       
   857 ML_file "Tools/bnf_tactics.ML"
       
   858 
   854 end
   859 end