src/Pure/Syntax/syntax_ext.ML
changeset 83029 d0da249ebd24
parent 81588 81a72b7fcb0c
equal deleted inserted replaced
83026:393a15735a60 83029:d0da249ebd24