equal
deleted
inserted
replaced
159 the type for the predicates and also returns typed terms for the |
159 the type for the predicates and also returns typed terms for the |
160 introduction rules. So at the heart of the function |
160 introduction rules. So at the heart of the function |
161 @{text "add_inductive_cmd"} is a call to @{ML read_spec in Specification}. |
161 @{text "add_inductive_cmd"} is a call to @{ML read_spec in Specification}. |
162 *} |
162 *} |
163 |
163 |
164 ML_val{*fun add_inductive_cmd pred_specs rule_specs lthy = |
164 ML_val%grayML{*fun add_inductive_cmd pred_specs rule_specs lthy = |
165 let |
165 let |
166 val ((pred_specs', rule_specs'), _) = |
166 val ((pred_specs', rule_specs'), _) = |
167 Specification.read_spec pred_specs rule_specs lthy |
167 Specification.read_spec pred_specs rule_specs lthy |
168 in |
168 in |
169 add_inductive pred_specs' rule_specs' lthy |
169 add_inductive pred_specs' rule_specs' lthy |