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/SetInterval.thy
changeset 33434 e9de8d69c1b9
parent 33318 ddd97d9dfbfb
child 35115 446c5063e4fd 
--- a/src/HOL/SetInterval.thy	Wed Nov 04 09:18:46 2009 +0100
+++ b/src/HOL/SetInterval.thy	Wed Nov 04 10:17:43 2009 +0100
@@ -508,7 +508,7 @@
   proof(induct A rule:finite_linorder_max_induct)
     case empty thus ?case by auto
   next
-    case (insert A b)
+    case (insert b A)
     moreover hence "b ~: A" by auto
     moreover have "A <= {k..<k+card A}" and "b = k+card A"
       using `b ~: A` insert by fastsimp+
isabelle