changeset 12050 | 6934c005aec4 |
parent 8813 | abc0f3722aed |
child 12132 | 1ef58b332ca9 |
--- a/src/ZF/thy_syntax.ML Sun Nov 04 21:00:28 2001 +0100 +++ b/src/ZF/thy_syntax.ML Sun Nov 04 21:12:03 2001 +0100 @@ -3,13 +3,11 @@ Author: Lawrence C Paulson Copyright 1994 University of Cambridge -Additional theory file sections for ZF. +Additional sections for *old-style* theory files in ZF. *) - local - open ThyParse; (*ML identifiers for introduction rules.*)