| changeset 1308 | 80dabcaafc38 |
| parent 1303 | c28403308b34 |
| child 1314 | 6d851952799c |
| 1304:dc65319809cc | 1308:80dabcaafc38 |
|---|---|
173 in |
173 in |
174 map (fn x => mp OF [x]) (HOLogic.conj_elims thm) |
174 map (fn x => mp OF [x]) (HOLogic.conj_elims thm) |
175 end |
175 end |
176 *} |
176 *} |
177 |
177 |
178 ML {* |
|
179 fun build_bv_eqvt perms simps inducts (t, n) = |
|
180 build_eqvts Binding.empty [t] [nth perms n] simps (nth inducts n) |
|
181 *} |
|
182 |
|
178 end |
183 end |