src/Pure/Syntax/syn_trans.ML
changeset 20854 f9cf9e62d11c
parent 20202 87205ea2af06
child 21535 07f8cd0d7962