src/Pure/ROOT.ML
changeset 24908 c74ad8782eeb
parent 24833 9131433b19bb
child 24963 c04ec061ac2b
equal deleted inserted replaced
24907:bfb2e82b61fe 24908:c74ad8782eeb