removed outdated comment;
authorwenzelm
Sun, 07 Jan 2001 21:35:11 +0100
changeset 10815 dd5fb02ff872
parent 10814 2ccc84b8f5a0
child 10816 8b2eafed6183
removed outdated comment;
src/Pure/drule.ML
--- a/src/Pure/drule.ML	Sun Jan 07 21:34:45 2001 +0100
+++ b/src/Pure/drule.ML	Sun Jan 07 21:35:11 2001 +0100
@@ -590,10 +590,6 @@
 
 (*(PROP ?phi ==> (!!x. PROP ?psi(x))) == (!!x. PROP ?phi ==> PROP ?psi(x))
   Rewrite rule for HHF normalization.
-
-  Note: the syntax of ProtoPure is insufficient to handle this
-  statement; storing it would be asking for trouble, e.g. when someone
-  tries to print the theory later.
 *)
 
 val norm_hhf_eq =