src/Pure/Syntax/term_position.ML
changeset 52861 e93d73b51fd0
parent 52175 626a757d3c2d
child 80873 e71cb37c7395
equal deleted inserted replaced
52860:f155c38242c1 52861:e93d73b51fd0