# 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";