src/HOL/Induct/Mutil.ML
changeset 8991 dc70b797827f
parent 8950 3e858b72fac9
child 9188 379b0c3f7c85