| changeset 59627 | bb1e4a35d506 |
| parent 59621 | 291934bac95e |
| child 59652 | 611d9791845f |
| 59626:a6e977d8b070 | 59627:bb1e4a35d506 |
|---|---|
77 |
77 |
78 in |
78 in |
79 |
79 |
80 fun mk_partial_elim_rules ctxt result = |
80 fun mk_partial_elim_rules ctxt result = |
81 let |
81 let |
82 val thy = Proof_Context.theory_of ctxt; |
|
83 |
|
84 val FunctionResult {fs, R, dom, psimps, cases, ...} = result; |
82 val FunctionResult {fs, R, dom, psimps, cases, ...} = result; |
85 val n_fs = length fs; |
83 val n_fs = length fs; |
86 |
84 |
87 fun mk_partial_elim_rule (idx, f) = |
85 fun mk_partial_elim_rule (idx, f) = |
88 let |
86 let |