src/Pure/Syntax/local_syntax.ML
changeset 49674 dbadb4d03cbc
parent 42290 b1f544c84040
child 51655 28d6eb23522c
equal deleted inserted replaced
49673:2a088cff1e7b 49674:dbadb4d03cbc