src/HOL/Ctr_Sugar.thy
changeset 55971 7644d63e8c3f
parent 55468 98b25c51e9e5
child 57631 959caab43a3d
     1.1 --- a/src/HOL/Ctr_Sugar.thy	Fri Mar 07 01:02:21 2014 +0100
     1.2 +++ b/src/HOL/Ctr_Sugar.thy	Fri Mar 07 10:22:27 2014 +0100
     1.3 @@ -27,7 +27,6 @@
     1.4  declare [[coercion_args case_elem - +]]
     1.5  
     1.6  ML_file "Tools/Ctr_Sugar/case_translation.ML"
     1.7 -setup Case_Translation.setup
     1.8  
     1.9  lemma iffI_np: "\<lbrakk>x \<Longrightarrow> \<not> y; \<not> x \<Longrightarrow> y\<rbrakk> \<Longrightarrow> \<not> x \<longleftrightarrow> y"
    1.10  by (erule iffI) (erule contrapos_pn)