thy_syntax.ML
changeset 230 e4cccc2dec54
parent 215 5f9d7ed4ea0c