src/Pure/Syntax/simple_syntax.ML
changeset 78430 0461fc9d43e8
parent 67721 5348bea4accd
child 81601 26ff119fb140
equal deleted inserted replaced
78429:103a81e60126 78430:0461fc9d43e8