src/Pure/pure_syn.ML
changeset 59140 e7f28b330cb2
parent 58999 ed09ae4ea2d8
child 60095 35f626b11422