src/Pure/Tools/am_util.ML
changeset 16809 8ca51a846576
parent 16781 663235466562
child 16842 5979c46853d1
equal deleted inserted replaced
16808:644fc45c7292 16809:8ca51a846576