src/HOL/Induct/Mutil.ML
changeset 4389 1865cb8df116
parent 4387 31d5a5a191e8
child 4477 b3e5857d8d99