src/Pure/pure_syn.ML
changeset 66475 d8e0fd64216f
parent 64556 851ae0e7b09c
child 67381 146757999c8d
equal deleted inserted replaced
66474:3ff851a8cb4b 66475:d8e0fd64216f