# HG changeset patch
# User mueller
# Date 816617436 -3600
# Node ID f6651b6b0482d5b6f25ecc93fea9b287c4aab1a8
# Parent  69fec018854c59c862c34e08a6f9d1e9123118dc
*** empty log message ***

diff -r 69fec018854c -r f6651b6b0482 src/HOL/IOA/NTP/Correctness.ML
--- a/src/HOL/IOA/NTP/Correctness.ML	Fri Nov 17 13:22:50 1995 +0100
+++ b/src/HOL/IOA/NTP/Correctness.ML	Fri Nov 17 15:10:36 1995 +0100
@@ -117,4 +117,4 @@
 by(fast_tac (HOL_cs addSDs [add_leD1 RS leD]) 1);
 
 by(Asm_full_simp_tac 1);
-result();
+qed"ntp_correct";