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.
NEWS
changeset 18248 929659a46ecf
parent 18239 7607500220da
child 18267 5ee688e36eeb 
--- a/NEWS	Fri Nov 25 17:41:52 2005 +0100
+++ b/NEWS	Fri Nov 25 18:58:34 2005 +0100
@@ -78,10 +78,10 @@
     shows "P n x"
     using a                     -- {* make induct insert fact a *}
   proof (induct n fixing: x)    -- {* generalize goal to "!!x. A n x ==> P n x" *}
-    case (0 x)
+    case 0
     show ?case sorry
   next
-    case (Suc n x)
+    case (Suc n)
     note `!!x. A n x ==> P n x` -- {* induction hypothesis, according to induction rule *}
     note `A (Suc n) x`          -- {* induction premise, stemming from fact a *}
     show ?case sorry
isabelle