equal
deleted
inserted
replaced
28 declare [[coercion_args case_elem - +]] |
28 declare [[coercion_args case_elem - +]] |
29 |
29 |
30 ML_file "Tools/Ctr_Sugar/case_translation.ML" |
30 ML_file "Tools/Ctr_Sugar/case_translation.ML" |
31 |
31 |
32 lemma iffI_np: "\<lbrakk>x \<Longrightarrow> \<not> y; \<not> x \<Longrightarrow> y\<rbrakk> \<Longrightarrow> \<not> x \<longleftrightarrow> y" |
32 lemma iffI_np: "\<lbrakk>x \<Longrightarrow> \<not> y; \<not> x \<Longrightarrow> y\<rbrakk> \<Longrightarrow> \<not> x \<longleftrightarrow> y" |
33 by (erule iffI) (erule contrapos_pn) |
33 by (erule iffI) (erule contrapos_pn) |
34 |
34 |
35 lemma iff_contradict: |
35 lemma iff_contradict: |
36 "\<not> P \<Longrightarrow> P \<longleftrightarrow> Q \<Longrightarrow> Q \<Longrightarrow> R" |
36 "\<not> P \<Longrightarrow> P \<longleftrightarrow> Q \<Longrightarrow> Q \<Longrightarrow> R" |
37 "\<not> Q \<Longrightarrow> P \<longleftrightarrow> Q \<Longrightarrow> P \<Longrightarrow> R" |
37 "\<not> Q \<Longrightarrow> P \<longleftrightarrow> Q \<Longrightarrow> P \<Longrightarrow> R" |
38 by blast+ |
38 by blast+ |
39 |
39 |
40 ML_file "Tools/Ctr_Sugar/local_interpretation.ML" |
40 ML_file "Tools/Ctr_Sugar/local_interpretation.ML" |
41 ML_file "Tools/Ctr_Sugar/ctr_sugar_util.ML" |
41 ML_file "Tools/Ctr_Sugar/ctr_sugar_util.ML" |
42 ML_file "Tools/Ctr_Sugar/ctr_sugar_tactics.ML" |
42 ML_file "Tools/Ctr_Sugar/ctr_sugar_tactics.ML" |
43 ML_file "Tools/Ctr_Sugar/ctr_sugar_code.ML" |
43 ML_file "Tools/Ctr_Sugar/ctr_sugar_code.ML" |