src/HOL/Induct/ROOT.ML
changeset 10168 50be659d4222
parent 9951 5610c4acb48d
child 10259 93ec82d535f2