src/Pure/Syntax/syntax_phases.ML
changeset 69446 9cf0b79dfb7f
parent 69042 6e9df530b441
child 70784 799437173553
equal deleted inserted replaced
69445:bff0011cdf42 69446:9cf0b79dfb7f