QuotMain.thy
changeset 503 d2c9a72e52e0
parent 502 6b2f6e7e62cc
child 505 6cdba30c6d66
equal deleted inserted replaced
502:6b2f6e7e62cc 503:d2c9a72e52e0
   714 *}
   714 *}
   715 
   715 
   716 section {* RepAbs Injection Tactic *}
   716 section {* RepAbs Injection Tactic *}
   717 
   717 
   718 (* TODO: check if it still works with first_order_match *)
   718 (* TODO: check if it still works with first_order_match *)
   719 (* FIXME/TODO: do not handle everything *)x
   719 (* FIXME/TODO: do not handle everything *)
   720 ML {*
   720 ML {*
   721 fun instantiate_tac thm = 
   721 fun instantiate_tac thm = 
   722   Subgoal.FOCUS (fn {concl, ...} =>
   722   Subgoal.FOCUS (fn {concl, ...} =>
   723   let
   723   let
   724     val pat = Drule.strip_imp_concl (cprop_of thm)
   724     val pat = Drule.strip_imp_concl (cprop_of thm)