summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Wellfounded.thy

changeset 49945 | fb696ff1f086 |

parent 48891 | c0eafbd55de3 |

child 54295 | 45a5523d4a63 |

1.1 --- a/src/HOL/Wellfounded.thy Sat Oct 20 09:09:33 2012 +0200 1.2 +++ b/src/HOL/Wellfounded.thy Sat Oct 20 09:09:34 2012 +0200 1.3 @@ -764,9 +764,9 @@ 1.4 with Mw show "?N2 \<in> ?W" by (simp only:) 1.5 next 1.6 assume "M \<noteq> {}" 1.7 - have N2: "(?N2, M) \<in> max_ext r" 1.8 - by (rule max_extI[OF _ _ `M \<noteq> {}`]) (insert asm1, auto intro: finites) 1.9 - 1.10 + from asm1 finites have N2: "(?N2, M) \<in> max_ext r" 1.11 + by (rule_tac max_extI[OF _ _ `M \<noteq> {}`]) auto 1.12 + 1.13 with `M \<in> ?W` show "?N2 \<in> ?W" by (rule acc_downward) 1.14 qed 1.15 with finites have "?N1 \<union> ?N2 \<in> ?W"