src/Pure/Syntax/syn_trans.ML
changeset 9841 ca3173f87b5c
parent 8595 06874c5c3cfa
child 10572 b070825579b8