Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Wellfounded.thy
changeset 63982 4c4049e3bad8
parent 63915 bab633745c7f
child 64632 9df24b8b6c0a 
--- a/src/HOL/Wellfounded.thy	Sat Oct 01 19:29:48 2016 +0200
+++ b/src/HOL/Wellfounded.thy	Sat Oct 01 19:30:21 2016 +0200
@@ -837,8 +837,9 @@
       qed
     qed
   next
-    case [simp]: infinite
-    show ?case by (rule accI) (auto elim: max_ext.cases)
+    case infinite
+    show ?case
+      by (rule accI) (auto elim: max_ext.cases simp: infinite)
   qed
 qed
isabelle