# HG changeset patch
# User nipkow
# Date 860493839 -7200
# Node ID feab36851df36e5126f89801dedb185b1394dcb6
# Parent  953a47dc0519ae14fa2b4691e5826688bad6f7f1
Couldn't solve n < n+1 because of missing -1

diff -r 953a47dc0519 -r feab36851df3 src/Provers/nat_transitive.ML
--- a/src/Provers/nat_transitive.ML	Tue Apr 08 10:48:42 1997 +0200
+++ b/src/Provers/nat_transitive.ML	Tue Apr 08 12:03:59 1997 +0200
@@ -178,7 +178,7 @@
 (* recognize and solve trivial goal *)
 fun triv_sol(x,i,y,j,_) =
   if x=y andalso i<j
-  then Some(Incr1(Incr2(Thm([],Less.lessI),i),j-i)) else
+  then Some(Incr1(Incr2(Thm([],Less.lessI),i),j-i-1)) else
   if Less.is_zero(x) andalso i<j
   then Some(Incr1(Incr2(Thm([],Less.zero_less_Suc),i),j-i-1))
   else None;