src/Provers/quantifier1.ML
changeset 72142 3956d85e8e81
parent 72112 4f4695757980
child 72143 435cdc772110
equal deleted inserted replaced
72141:3867734b9a40 72142:3956d85e8e81
   185       tac ctxt,
   185       tac ctxt,
   186       tac ctxt];
   186       tac ctxt];
   187   fun prove_one_point_all_tac ctxt =
   187   fun prove_one_point_all_tac ctxt =
   188     EVERY1 [qcomm_tac ctxt All_comm @{thm equal_allI},
   188     EVERY1 [qcomm_tac ctxt All_comm @{thm equal_allI},
   189       resolve_tac ctxt [@{thm equal_allI}],
   189       resolve_tac ctxt [@{thm equal_allI}],
       
   190       Object_Logic.full_atomize_tac ctxt,
   190       resolve_tac ctxt [@{thm equal_intr_rule}],
   191       resolve_tac ctxt [@{thm equal_intr_rule}],
   191       Object_Logic.atomize_prems_tac ctxt,
       
   192       tac ctxt,
   192       tac ctxt,
   193       Object_Logic.atomize_prems_tac ctxt,
       
   194       tac ctxt];
   193       tac ctxt];
   195 end
   194 end
   196 
   195 
   197 fun prove_conv ctxt tu tac =
   196 fun prove_conv ctxt tu tac =
   198   let
   197   let