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 32006 0e209ff7f236
parent 31998 2c7a24f74db9
child 32400 6c62363cf0d7 
--- a/src/HOL/SetInterval.thy	Wed Jul 15 12:44:41 2009 +0200
+++ b/src/HOL/SetInterval.thy	Wed Jul 15 15:09:33 2009 +0200
@@ -425,7 +425,7 @@
 proof cases
   assume "finite A"
   thus "PROP ?P"
-  proof(induct A rule:finite_linorder_induct)
+  proof(induct A rule:finite_linorder_max_induct)
     case empty thus ?case by auto
   next
     case (insert A b)
isabelle