equal
deleted
inserted
replaced
67 val rsp_thms = map (fn gl => Goal.prove ctxt [] [] gl tac) rsp_goals |
67 val rsp_thms = map (fn gl => Goal.prove ctxt [] [] gl tac) rsp_goals |
68 in |
68 in |
69 ctxt |
69 ctxt |
70 |> snd o Local_Theory.note |
70 |> snd o Local_Theory.note |
71 ((Binding.empty, [Attrib.internal (fn _ => Quotient_Info.rsp_rules_add)]), rsp_thms) |
71 ((Binding.empty, [Attrib.internal (fn _ => Quotient_Info.rsp_rules_add)]), rsp_thms) |
72 |> snd o Local_Theory.note ((bind, []), user_thms) |
72 |> Local_Theory.note ((bind, []), user_thms) |
73 end |
73 end |
74 *} |
74 *} |
75 |
75 |
76 |
76 |
77 |
77 |
97 )) |
97 )) |
98 end |
98 end |
99 *} |
99 *} |
100 |
100 |
101 (* Testing code |
101 (* Testing code |
102 local_setup {* prove_const_rsp @{binding fv_rtrm2_rsp} [@{term rbv2}] |
102 local_setup {* snd o prove_const_rsp @{binding fv_rtrm2_rsp} [@{term rbv2}] |
103 (fn _ => fv_rsp_tac @{thm alpha_rtrm2_alpha_rassign.inducts(2)} @{thms fv_rtrm2_fv_rassign.simps} 1) *}*) |
103 (fn _ => fv_rsp_tac @{thm alpha_rtrm2_alpha_rassign.inducts(2)} @{thms fv_rtrm2_fv_rassign.simps} 1) *}*) |
104 |
104 |
105 (*ML {* |
105 (*ML {* |
106 val rsp_goals = map (const_rsp @{context}) [@{term rbv2}] |
106 val rsp_goals = map (const_rsp @{context}) [@{term rbv2}] |
107 val (fixed, user_goals) = split_list (map (get_rsp_goal @{theory}) rsp_goals) |
107 val (fixed, user_goals) = split_list (map (get_rsp_goal @{theory}) rsp_goals) |