src/Pure/Isar/local_syntax.ML
changeset 35205 611b90bb89bc
parent 33387 acea2f336721
child 35412 b8dead547d9e
equal deleted inserted replaced
35204:214ec053128e 35205:611b90bb89bc