src/HOL/IMPP/ROOT.ML
changeset 24355 93d78fdeb55a
parent 9000 c20d58286a51
child 33615 261abc2e3155
equal deleted inserted replaced
24354:0fdabe28f0e6 24355:93d78fdeb55a