| changeset 1313 | da44ef9a7df2 |
| parent 1308 | 80dabcaafc38 |
| child 1314 | 6d851952799c |
| 1312:b0eae8c93314 | 1313:da44ef9a7df2 |
|---|---|
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 |