src/Pure/Syntax/simple_syntax.ML
changeset 81656 7593c0976dc6
parent 81601 26ff119fb140