thy_syntax.ML
changeset 228 e2245da1b601
parent 215 5f9d7ed4ea0c