equal
deleted
inserted
replaced
356 val simp_set = @{thms atom_eqvt permute_list.simps} @ simps @ all_eqvts ctxt' |
356 val simp_set = @{thms atom_eqvt permute_list.simps} @ simps @ all_eqvts ctxt' |
357 val tac = asm_full_simp_tac (HOL_ss addsimps simp_set) |
357 val tac = asm_full_simp_tac (HOL_ss addsimps simp_set) |
358 val ths_loc = prove_by_induct tys (build_eqvt_gl p) ind tac funs ctxt' |
358 val ths_loc = prove_by_induct tys (build_eqvt_gl p) ind tac funs ctxt' |
359 val ths = Variable.export ctxt' ctxt ths_loc |
359 val ths = Variable.export ctxt' ctxt ths_loc |
360 val add_eqvt = Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add) |
360 val add_eqvt = Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add) |
|
361 val _ = tracing ("eqvt thms\n" ^ cat_lines (map (Syntax.string_of_term ctxt o prop_of) ths)) |
361 in |
362 in |
362 (ths, snd (Local_Theory.note ((Binding.empty, [add_eqvt]), ths) ctxt)) |
363 (ths, snd (Local_Theory.note ((Binding.empty, [add_eqvt]), ths) ctxt)) |
363 end |
364 end |
364 *} |
365 *} |
365 |
366 |