src/HOL/ex/ROOT.ML
changeset 8421 7156b8e26a17
parent 8353 57a163920480
child 8557 fe75fe482566
equal deleted inserted replaced
8420:f37fd19476ca 8421:7156b8e26a17