src/HOL/Ctr_Sugar.thy
changeset 58188 cc71d2be4f0a
parent 58177 166131276380
child 58659 6c9821c32dd5
     1.1 --- a/src/HOL/Ctr_Sugar.thy	Fri Sep 05 00:41:01 2014 +0200
     1.2 +++ b/src/HOL/Ctr_Sugar.thy	Fri Sep 05 00:41:01 2014 +0200
     1.3 @@ -30,12 +30,12 @@
     1.4  ML_file "Tools/Ctr_Sugar/case_translation.ML"
     1.5  
     1.6  lemma iffI_np: "\<lbrakk>x \<Longrightarrow> \<not> y; \<not> x \<Longrightarrow> y\<rbrakk> \<Longrightarrow> \<not> x \<longleftrightarrow> y"
     1.7 -by (erule iffI) (erule contrapos_pn)
     1.8 +  by (erule iffI) (erule contrapos_pn)
     1.9  
    1.10  lemma iff_contradict:
    1.11 -"\<not> P \<Longrightarrow> P \<longleftrightarrow> Q \<Longrightarrow> Q \<Longrightarrow> R"
    1.12 -"\<not> Q \<Longrightarrow> P \<longleftrightarrow> Q \<Longrightarrow> P \<Longrightarrow> R"
    1.13 -by blast+
    1.14 +  "\<not> P \<Longrightarrow> P \<longleftrightarrow> Q \<Longrightarrow> Q \<Longrightarrow> R"
    1.15 +  "\<not> Q \<Longrightarrow> P \<longleftrightarrow> Q \<Longrightarrow> P \<Longrightarrow> R"
    1.16 +  by blast+
    1.17  
    1.18  ML_file "Tools/Ctr_Sugar/local_interpretation.ML"
    1.19  ML_file "Tools/Ctr_Sugar/ctr_sugar_util.ML"