src/Pure/Isar/element.ML
changeset 78577 a945b541efff
parent 78453 3fdf3c5cfa9d
child 80306 c2537860ccf8