# HG changeset patch
# User wenzelm
# Date 970491483 -7200
# Node ID 1d428e8915722c3b95157c5f3f84b7aecc6cab90
# Parent  82adc50ee7c2ba8d987e4595281f0057807a5aaa
qed "";

diff -r 82adc50ee7c2 -r 1d428e891572 src/HOL/ex/svc_test.ML
--- a/src/HOL/ex/svc_test.ML	Mon Oct 02 14:57:46 2000 +0200
+++ b/src/HOL/ex/svc_test.ML	Mon Oct 02 14:58:03 2000 +0200
@@ -16,7 +16,7 @@
   in its length, though Fast_tac manages*)
 Goal "P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P";
 by (svc_tac 1);
-result();
+qed "";
 
 (** Some big tautologies supplied by John Harrison **)
 
@@ -43,7 +43,7 @@
 \  (~v7 | ~v8 | v9) & \
 \  (~v10 | ~v11 | v12))";
 by (svc_tac 1);
-result();
+qed "";
 
 (*Tautology name: dk17_be*)
 Goal "(GE17 <-> ~IN4 & ~IN3 & ~IN2 & ~IN1) & \
@@ -122,7 +122,7 @@
 \       (OUT1 <-> WRES7 & IN8) & \
 \       (OUT0 <-> WRES7 & ~IN8)";
 by (svc_tac 1);
-result();
+qed "";
 
 (*Tautology name: sqn_be.  Fast_tac only takes a couple of seconds.*)
 Goal "(GE0 <-> IN6 & IN1 | ~IN6 & ~IN1) & \
@@ -226,7 +226,7 @@
 \       WRES18 & WRES0 & ~IN5 | \
 \       WRES19)";
 by (svc_tac 1);
-result();
+qed "";
 
 
 (** Linear arithmetic **)
@@ -235,20 +235,20 @@
 \     x ~= #8 & x ~= #7 & x ~= #6 & x ~= #5 & x ~= #4 & x ~= #3 & \
 \     x ~= #2 & x ~= #1 & #0 < x & x < #16 --> #15 = (x::int)";
 by (svc_tac 1);
-result();
+qed "";
 
 (*merely to test polarity handling in the presence of biconditionals*)
 Goal "(x < (y::int)) = (x+#1 <= y)";
 by (svc_tac 1);
-result();
+qed "";
 
 (** Natural number examples requiring implicit "non-negative" assumptions*)
 
 Goal "(#3::nat)*a <= #2 + #4*b + #6*c  & #11 <= #2*a + b + #2*c & \
 \     a + #3*b <= #5 + #2*c  --> #2 + #3*b <= #2*a + #6*c";
 by (svc_tac 1);
-result();
+qed "";
 
 Goal "(n::nat) < #2 ==> (n = #0) | (n = #1)";
 by (svc_tac 1);
-result();
+qed "";