src/Pure/Isar/element.ML
changeset 80870 9a7de3f320d8
parent 80706 29734511c661
equal deleted inserted replaced
80869:87395be1a299 80870:9a7de3f320d8