src/Pure/General/source.ML
changeset 16608 4f8d7b83c7e2
parent 15531 08c8dad8e399
child 19485 5385c9d86c2a
equal deleted inserted replaced
16607:81e687c63e29 16608:4f8d7b83c7e2