src/HOL/thy_syntax.ML
changeset 6378 5780d71203bb
parent 6356 6c01697e082e
child 6381 ed0c7b4a325d