thy_syntax.ML
changeset 231 31040e4345e8
parent 215 5f9d7ed4ea0c