# HG changeset patch
# User wenzelm
# Date 1004217679 -7200
# Node ID bd0111191d71c79248b49988a832eb248f7aca15
# Parent  15da572c3c2710401f61a4ffcaa29c875fa8eaf5
tuned;

diff -r 15da572c3c27 -r bd0111191d71 src/HOL/HOL_lemmas.ML
--- a/src/HOL/HOL_lemmas.ML	Sat Oct 27 23:19:55 2001 +0200
+++ b/src/HOL/HOL_lemmas.ML	Sat Oct 27 23:21:19 2001 +0200
@@ -6,7 +6,7 @@
 Derived rules from Appendix of Mike Gordons HOL Report, Cambridge TR 68.
 *)
 
-(* ML bindings *)
+(* legacy ML bindings *)
 
 val plusI = thm "plusI";
 val minusI = thm "minusI";