equal
deleted
inserted
replaced
745 by (rule classical) iprover |
745 by (rule classical) iprover |
746 |
746 |
747 lemma swap: "\<not> P \<Longrightarrow> (\<not> R \<Longrightarrow> P) \<Longrightarrow> R" |
747 lemma swap: "\<not> P \<Longrightarrow> (\<not> R \<Longrightarrow> P) \<Longrightarrow> R" |
748 by (rule classical) iprover |
748 by (rule classical) iprover |
749 |
749 |
750 lemma thin_refl: "\<And>X. \<lbrakk>x = x; PROP W\<rbrakk> \<Longrightarrow> PROP W" . |
750 lemma thin_refl: "\<lbrakk>x = x; PROP W\<rbrakk> \<Longrightarrow> PROP W" . |
751 |
751 |
752 ML \<open> |
752 ML \<open> |
753 structure Hypsubst = Hypsubst |
753 structure Hypsubst = Hypsubst |
754 ( |
754 ( |
755 val dest_eq = HOLogic.dest_eq |
755 val dest_eq = HOLogic.dest_eq |
1504 |
1504 |
1505 lemma [induct_simp]: "(PROP P \<Longrightarrow> induct_true) \<equiv> Trueprop induct_true" |
1505 lemma [induct_simp]: "(PROP P \<Longrightarrow> induct_true) \<equiv> Trueprop induct_true" |
1506 unfolding induct_true_def |
1506 unfolding induct_true_def |
1507 by (iprover intro: equal_intr_rule) |
1507 by (iprover intro: equal_intr_rule) |
1508 |
1508 |
1509 lemma [induct_simp]: "(\<And>x. induct_true) \<equiv> Trueprop induct_true" |
1509 lemma [induct_simp]: "(\<And>x::'a::{}. induct_true) \<equiv> Trueprop induct_true" |
1510 unfolding induct_true_def |
1510 unfolding induct_true_def |
1511 by (iprover intro: equal_intr_rule) |
1511 by (iprover intro: equal_intr_rule) |
1512 |
1512 |
1513 lemma [induct_simp]: "induct_implies induct_true P \<equiv> P" |
1513 lemma [induct_simp]: "induct_implies induct_true P \<equiv> P" |
1514 by (simp add: induct_implies_def induct_true_def) |
1514 by (simp add: induct_implies_def induct_true_def) |