src/Pure/Isar/outer_syntax.ML
changeset 49283 97809ae5f7bb
parent 48992 0518bf89c777
child 49564 03381c41235b
equal deleted inserted replaced
49282:c057e1b39f16 49283:97809ae5f7bb