src/Pure/Thy/thy_syntax.ML
changeset 31338 d41a8ba25b67
parent 30573 49899f26fbd1
child 36950 75b8f26f2f07
equal deleted inserted replaced
31337:a9ed5fcc5e39 31338:d41a8ba25b67