src/Pure/context_position.ML
changeset 82583 abd3885a3fcf
parent 80868 0ed02f473cf9
equal deleted inserted replaced
82582:bcee022fbe30 82583:abd3885a3fcf