equal
deleted
inserted
replaced
27 --| Args.$$$ ":"; |
27 --| Args.$$$ ":"; |
28 |
28 |
29 |
29 |
30 (* induct_rule *) |
30 (* induct_rule *) |
31 |
31 |
32 fun kind_rule Type = (#induction oo DatatypePackage.datatype_info, Sign.intern_tycon) |
32 fun kind_rule Type = (#induction oo DatatypePackage.datatype_info_err, Sign.intern_tycon) |
33 | kind_rule Set = ((#induct o #2) oo InductivePackage.get_inductive, Sign.intern_const) |
33 | kind_rule Set = ((#induct o #2) oo InductivePackage.get_inductive, Sign.intern_const) |
34 | kind_rule Function = (#induct oo RecdefPackage.get_recdef, Sign.intern_const); |
34 | kind_rule Function = (#induct oo RecdefPackage.get_recdef, Sign.intern_const); |
35 |
35 |
36 fun induct_rule thy kind name = |
36 fun induct_rule thy kind name = |
37 let val (ind_rule, intern) = kind_rule kind |
37 let val (ind_rule, intern) = kind_rule kind |