src/HOL/Tools/induct_method.ML
changeset 10445 59265527d9eb
parent 10439 be2dc95dfe98
child 10455 acfdc430f4cd