summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | blanchet |

Thu, 16 Jan 2014 18:37:37 +0100 | |

changeset 55021 | e40090032de9 |

parent 55020 | 96b05fd2aee4 |

child 55022 | eeba3ba73486 |

compile (importing 'Metis' or 'Main' would have been an alternative)

--- a/src/HOL/Cardinals/Order_Union.thy Thu Jan 16 18:26:41 2014 +0100 +++ b/src/HOL/Cardinals/Order_Union.thy Thu Jan 16 18:37:37 2014 +0100 @@ -31,7 +31,7 @@ assume Case1: "B \<noteq> {}" hence "B \<noteq> {} \<and> B \<le> Field r" using B_def by auto then obtain a where 1: "a \<in> B" and 2: "\<forall>a1 \<in> B. (a1,a) \<notin> r" - using WF unfolding wf_eq_minimal2 by metis + using WF unfolding wf_eq_minimal2 by blast hence 3: "a \<in> Field r \<and> a \<notin> Field r'" using B_def FLD by auto (* *) have "\<forall>a1 \<in> A. (a1,a) \<notin> r Osum r'" @@ -59,7 +59,7 @@ assume Case2: "B = {}" hence 1: "A \<noteq> {} \<and> A \<le> Field r'" using * ** B_def by auto then obtain a' where 2: "a' \<in> A" and 3: "\<forall>a1' \<in> A. (a1',a') \<notin> r'" - using WF' unfolding wf_eq_minimal2 by metis + using WF' unfolding wf_eq_minimal2 by blast hence 4: "a' \<in> Field r' \<and> a' \<notin> Field r" using 1 FLD by blast (* *) have "\<forall>a1' \<in> A. (a1',a') \<notin> r Osum r'" @@ -338,7 +338,7 @@ using 1 WF' wf_Un[of "Field r \<times> Field r'" "r' - Id"] by (auto simp add: Un_commute) } - ultimately have ?thesis by (metis wf_subset) + ultimately have ?thesis using wf_subset by blast } moreover {assume Case22: "r' \<le> Id" @@ -351,7 +351,7 @@ using 1 WF wf_Un[of "r - Id" "Field r \<times> Field r'"] by (auto simp add: Un_commute) } - ultimately have ?thesis by (metis wf_subset) + ultimately have ?thesis using wf_subset by blast } ultimately show ?thesis by blast qed