src/Pure/pure_syn.ML
changeset 71218 73b313432d8a
parent 69965 da5e7278286b
child 73751 fefb5ccb1e5e
equal deleted inserted replaced
71217:2dee5cd42fde 71218:73b313432d8a