equal
deleted
inserted
replaced
81 val (op ==>) = Logic.mk_implies; |
81 val (op ==>) = Logic.mk_implies; |
82 |
82 |
83 |
83 |
84 (* attributes *) |
84 (* attributes *) |
85 |
85 |
86 val case_names_fields = RuleCases.case_names ["fields"]; |
86 fun case_names_fields x = RuleCases.case_names ["fields"] x; |
87 fun induct_type_global name = [case_names_fields, InductAttrib.induct_type_global name]; |
87 fun induct_type_global name = [case_names_fields, InductAttrib.induct_type_global name]; |
88 fun cases_type_global name = [case_names_fields, InductAttrib.cases_type_global name]; |
88 fun cases_type_global name = [case_names_fields, InductAttrib.cases_type_global name]; |
89 |
89 |
90 |
90 |
91 (* tactics *) |
91 (* tactics *) |