equal
deleted
inserted
replaced
207 val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj gls) |
207 val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj gls) |
208 val thm = Goal.prove ctxt names [] gl tac |
208 val thm = Goal.prove ctxt names [] gl tac |
209 in |
209 in |
210 map (fn x => mp OF [x]) (HOLogic.conj_elims thm) |
210 map (fn x => mp OF [x]) (HOLogic.conj_elims thm) |
211 end |
211 end |
212 *} |
|
213 |
|
214 ML {* |
|
215 fun build_bv_eqvt simps inducts (t, n) ctxt = |
|
216 build_eqvts Binding.empty [t] (build_eqvts_tac (nth inducts n) simps ctxt) ctxt |
|
217 *} |
212 *} |
218 |
213 |
219 ML {* |
214 ML {* |
220 fun prove_fv_rsp fv_alphas_lst all_alphas tac ctxt = |
215 fun prove_fv_rsp fv_alphas_lst all_alphas tac ctxt = |
221 let |
216 let |