src/HOL/Hoare/Arith2.ML

 (*** HOL lemmas ***)
 
 
 val [prem1,prem2]=goal HOL.thy "[|~P ==> ~Q; Q|] ==> P";
 by (cut_facts_tac [prem1 COMP impI,prem2] 1);
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
 val not_imp_swap=result();
 
 
 (*** analogue of diff_induct, for simultaneous induction over 3 vars ***)
 

 br allI 7;
 by (nat_ind_tac "xa" 7);
 by (ALLGOALS (resolve_tac prems));
 ba 1;
 ba 1;
-by (fast_tac HOL_cs 1);
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
+by (Fast_tac 1);
 qed "diff_induct3";
 
 (*** interaction of + and - ***)
 
 val prems=goal Arith.thy "~m<n+k ==> (m - n) - k = m - ((n + k)::nat)";

 (*
 val prems = goal thy "0<n ==> n mod n = 0";
 by (cut_inst_tac [("m","Suc(0)")] (mod_prod_nn_is_0 COMP impI) 1);
 by (cut_facts_tac prems 1);
 by (Asm_full_simp_tac 1);
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
 *)
 
 val prems=goal thy "0<n ==> n mod n = 0";
 by (cut_facts_tac prems 1);
 br (mod_def RS wf_less_trans) 1;

 bd divides_le 1;
 by (Asm_simp_tac 1);
 qed "cd_le";
 
 val prems=goalw thy [cd_def] "cd x m n = cd x n m";
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
 qed "cd_swap";
 
 val prems=goalw thy [cd_def] "n<m ==> cd x m n = cd x (m-n) n";
 by (cut_facts_tac prems 1);
 br iffI 1;