src/Pure/pure_thy.ML
changeset 9744 9ca034ef256c
parent 9564 391f3ee75b1e
child 9808 4e47e40c0ac5
equal deleted inserted replaced
9743:d18d5c4a1f80 9744:9ca034ef256c