Nominal/Rsp.thy
changeset 1278 8814494fe4da
parent 1268 d1999540d23a
child 1300 22a084c9316b
equal deleted inserted replaced
1277:6eacf60ce41d 1278:8814494fe4da
    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)