equal
deleted
inserted
replaced
131 fun map7 _ [] [] [] [] [] [] [] = [] |
131 fun map7 _ [] [] [] [] [] [] [] = [] |
132 | map7 f (x :: xs) (y :: ys) (z :: zs) (u :: us) (v :: vs) (r :: rs) (s :: ss) = |
132 | map7 f (x :: xs) (y :: ys) (z :: zs) (u :: us) (v :: vs) (r :: rs) (s :: ss) = |
133 f x y z u v r s :: map7 f xs ys zs us vs rs ss |
133 f x y z u v r s :: map7 f xs ys zs us vs rs ss |
134 |
134 |
135 (* local abbreviations *) |
135 (* local abbreviations *) |
136 fun eqvt_stac ctxt = Nominal_Permeq.eqvt_strict_tac ctxt @{thms permute_minus_cancel} [] |
136 |
137 fun eqvt_srule ctxt = Nominal_Permeq.eqvt_strict_rule ctxt @{thms permute_minus_cancel} [] |
137 local |
|
138 open Nominal_Permeq |
|
139 in |
|
140 (* by default eqvt_strict_config contains unwanted @{thm permute_pure} *) |
|
141 |
|
142 val eqvt_sconfig = (delposts eqvt_strict_config) addpres @{thms permute_minus_cancel} |
|
143 |
|
144 fun eqvt_stac ctxt = eqvt_tac ctxt eqvt_sconfig |
|
145 fun eqvt_srule ctxt = eqvt_rule ctxt eqvt_sconfig |
|
146 |
|
147 end |
138 |
148 |
139 val all_elims = |
149 val all_elims = |
140 let |
150 let |
141 fun spec' ct = Drule.instantiate' [SOME (ctyp_of_term ct)] [NONE, SOME ct] @{thm spec} |
151 fun spec' ct = Drule.instantiate' [SOME (ctyp_of_term ct)] [NONE, SOME ct] @{thm spec} |
142 in |
152 in |