795         (Const(@{const_name Trueprop}, _) $ (Const (@{const_name QUOT_TRUE}, _) $ _)) => true

   795         (Const(@{const_name Trueprop}, _) $ (Const (@{const_name QUOT_TRUE}, _) $ _)) => true

   796       | _ => false

   796       | _ => false

   797   in

   797   in

   798     case find_first find_fun asms of

   798     case find_first find_fun asms of

   799       SOME (_ $ (_ $ (f $ a))) => (f, a)

   799       SOME (_ $ (_ $ (f $ a))) => (f, a)

   801   end

   802   end

   802 *}

   803 *}

   803 

   804 

   804 (* It proves the Quotient assumptions by calling quotient_tac *)

   805 (* It proves the Quotient assumptions by calling quotient_tac *)

   805 ML {*

   806 ML {*

   826 ML {*

   827 ML {*

   827 val apply_rsp_tac =

   828 val apply_rsp_tac =

   828   Subgoal.FOCUS (fn {concl, asms, context,...} =>

   829   Subgoal.FOCUS (fn {concl, asms, context,...} =>

   829     case ((HOLogic.dest_Trueprop (term_of concl))) of

   830     case ((HOLogic.dest_Trueprop (term_of concl))) of

   830       ((R2 $ (f $ x) $ (g $ y))) =>

   831       ((R2 $ (f $ x) $ (g $ y))) =>

   832           val (asmf, asma) = find_qt_asm (map term_of asms);

   833           val (asmf, asma) = find_qt_asm (map term_of asms);

   833         in

   834         in

   834           if (fastype_of asmf) = (fastype_of f) then no_tac else let

   835           if (fastype_of asmf) = (fastype_of f) then no_tac else let

   835             val ty_a = fastype_of x;

   836             val ty_a = fastype_of x;

   836             val ty_b = fastype_of asma;

   837             val ty_b = fastype_of asma;

   843             val thm = Drule.instantiate' [] t_inst te

   844             val thm = Drule.instantiate' [] t_inst te

   844           in

   845           in

   845             compose_tac (false, thm, 2) 1

   846             compose_tac (false, thm, 2) 1

   846           end

   847           end

   847         end

   848         end

   848     | _ => no_tac)

   850     | _ => no_tac)

   849 *}

   851 *}

   850 

   852 

   851 ML {*

   853 ML {*

   852 fun SOLVES' tac = tac THEN_ALL_NEW (fn _ => no_tac)

   854 fun SOLVES' tac = tac THEN_ALL_NEW (fn _ => no_tac)