src/Pure/Thy/thy_info.ML
changeset 12874 368966ceafe5
parent 10009 45c1eb3d8ad4
child 14774 d747c32e85e1
equal deleted inserted replaced
12873:d7f8dfaad46d 12874:368966ceafe5