src/Pure/Syntax/simple_syntax.ML
changeset 78086 5edd5b12017d
parent 67721 5348bea4accd
child 81601 26ff119fb140
equal deleted inserted replaced
78085:dd7bb7f99ad5 78086:5edd5b12017d