src/Provers/classical.ML
changeset 19877 705ba8232952
parent 19257 4463aee061bc
child 20956 00fe22000c6a
equal deleted inserted replaced
19876:11d447d5d68c 19877:705ba8232952
   194           then Tactic.etac thin_rl i
   194           then Tactic.etac thin_rl i
   195           else all_tac))
   195           else all_tac))
   196         |> Seq.hd
   196         |> Seq.hd
   197         |> Drule.zero_var_indexes
   197         |> Drule.zero_var_indexes
   198         |> Thm.put_name_tags (Thm.get_name_tags rule);
   198         |> Thm.put_name_tags (Thm.get_name_tags rule);
   199     in if Drule.weak_eq_thm (rule, rule'') then rule else rule'' end
   199     in if Drule.equiv_thm (rule, rule'') then rule else rule'' end
   200   else rule;
   200   else rule;
   201 
   201 
   202 
   202 
   203 
   203 
   204 (*** Useful tactics for classical reasoning ***)
   204 (*** Useful tactics for classical reasoning ***)