src/Pure/Syntax/syntax.ML
changeset 43826 2b094d17f432
parent 43731 70072780e095
child 44069 d7c7ec248ef0
equal deleted inserted replaced
43825:fbc3d9a3a6cd 43826:2b094d17f432