src/Pure/pure_thy.ML
changeset 7480 0a0e0dbe1269
parent 7470 9f67ca1e03dc
child 7485 31a25b6af1b3
equal deleted inserted replaced
7479:b482d827899c 7480:0a0e0dbe1269