author | wenzelm |
Sun, 07 Jan 2001 21:35:11 +0100 | |
changeset 10815 | dd5fb02ff872 |
parent 10814 | 2ccc84b8f5a0 |
child 10816 | 8b2eafed6183 |
src/Pure/drule.ML | file | annotate | diff | comparison | revisions |
--- 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 =