src/Pure/Syntax/syn_trans.ML
changeset 24547 64c20ee76bc1
parent 23963 c2ee97a963db
child 26424 a6cad32a27b0