src/HOL/Induct/ROOT.ML
changeset 4332 d4a15e32c024
parent 3120 c58423c20740
child 4449 df30e75f670f