src/Pure/Isar/local_syntax.ML
changeset 33126 bb8806eb5da7
parent 32738 15bb09ca0378
child 33387 acea2f336721
equal deleted inserted replaced
33125:2fef4f9429f7 33126:bb8806eb5da7