src/HOL/Induct/Mutil.ML
changeset 9369 139fde7af7bd
parent 9188 379b0c3f7c85
child 9930 c02d48a47ed1