src/Pure/pure_syn.ML
changeset 67013 335a7dce7cb3
parent 64556 851ae0e7b09c
child 67381 146757999c8d