src/Pure/Isar/outer_syntax.ML
changeset 15831 aa58e4ec3a1f
parent 15830 74d8412b1a27
child 15973 5fd94d84470f
equal deleted inserted replaced
15830:74d8412b1a27 15831:aa58e4ec3a1f