src/Pure/drule.ML
changeset 10815 dd5fb02ff872
parent 10767 8fa4aafa7314
child 11120 5254d35e4f7c
     1.1 --- a/src/Pure/drule.ML	Sun Jan 07 21:34:45 2001 +0100
     1.2 +++ b/src/Pure/drule.ML	Sun Jan 07 21:35:11 2001 +0100
     1.3 @@ -590,10 +590,6 @@
     1.4  
     1.5  (*(PROP ?phi ==> (!!x. PROP ?psi(x))) == (!!x. PROP ?phi ==> PROP ?psi(x))
     1.6    Rewrite rule for HHF normalization.
     1.7 -
     1.8 -  Note: the syntax of ProtoPure is insufficient to handle this
     1.9 -  statement; storing it would be asking for trouble, e.g. when someone
    1.10 -  tries to print the theory later.
    1.11  *)
    1.12  
    1.13  val norm_hhf_eq =