src/HOL/Real/RealDef.ML

 
 (**** real_minus: additive inverse on real ****)
 
 Goalw [congruent_def]
   "congruent realrel (%p. (%(x,y). realrel^^{(y,x)}) p)";
-by Safe_tac;
+by (Clarify_tac 1); 
 by (asm_full_simp_tac (simpset() addsimps [preal_add_commute]) 1);
 qed "real_minus_congruent";
 
 Goalw [real_minus_def]
       "- (Abs_real(realrel^^{(x,y)})) = Abs_real(realrel ^^ {(y,x)})";

 
 (*** Congruence property for addition ***)
 Goalw [congruent2_def]
     "congruent2 realrel (%p1 p2.                  \
 \         (%(x1,y1). (%(x2,y2). realrel^^{(x1+x2, y1+y2)}) p2) p1)";
-by Safe_tac;
+by (Clarify_tac 1); 
 by (asm_simp_tac (simpset() addsimps [preal_add_assoc]) 1);
 by (res_inst_tac [("z1.1","x1a")] (preal_add_left_commute RS ssubst) 1);
 by (asm_simp_tac (simpset() addsimps [preal_add_assoc RS sym]) 1);
 by (asm_simp_tac (simpset() addsimps preal_add_ac) 1);
 qed "real_add_congruent2";

 
 Goal 
     "congruent2 realrel (%p1 p2.                  \
 \         (%(x1,y1). (%(x2,y2). realrel^^{(x1*x2 + y1*y2, x1*y2+x2*y1)}) p2) p1)";
 by (rtac (equiv_realrel RS congruent2_commuteI) 1);
-by Safe_tac;
+by (Clarify_tac 1); 
 by (rewtac split_def);
 by (asm_simp_tac (simpset() addsimps [preal_mult_commute,preal_add_commute]) 1);
 by (auto_tac (claset(),simpset() addsimps [real_mult_congruent2_lemma]));
 qed "real_mult_congruent2";
 

 by (dtac real_less_trans 1 THEN assume_tac 1);
 by (asm_full_simp_tac (simpset() addsimps [real_less_not_refl]) 1);
 qed "real_less_not_sym";
 
 (* [| x < y;  ~P ==> y < x |] ==> P *)
-bind_thm ("real_less_asym", real_less_not_sym RS swap);
+bind_thm ("real_less_asym", real_less_not_sym RS contrapos_np);
 
 Goalw [real_of_preal_def] 
      "real_of_preal ((z1::preal) + z2) = \
 \     real_of_preal z1 + real_of_preal z2";
 by (asm_simp_tac (simpset() addsimps [real_add,