src/Pure/Thy/ROOT.ML
changeset 4945 d8c809afafb8
parent 4944 a6e71e5a1004
child 5013 5b0c97631aff
equal deleted inserted replaced
4944:a6e71e5a1004 4945:d8c809afafb8