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/Sequents/LK/Nat.thy
changeset 7123 4ab38de3fd20
parent 7095 cfc11af6174a
child 17481 75166ebb619b 
--- a/src/Sequents/LK/Nat.thy	Wed Jul 28 13:55:02 1999 +0200
+++ b/src/Sequents/LK/Nat.thy	Wed Jul 28 13:55:34 1999 +0200
@@ -16,7 +16,7 @@
 
 rules   
   induct  "[| $H |- $E, P(0), $F;
-              !!x. $H |- $E, P(x) --> P(Suc(x)), $F |] ==> $H |- $E, P(n), $F"
+              !!x. $H, P(x) |- $E, P(Suc(x)), $F |] ==> $H |- $E, P(n), $F"
 
   Suc_inject  "|- Suc(m)=Suc(n) --> m=n"
   Suc_neq_0   "|- Suc(m) ~= 0"
isabelle