src/HOL/Nat.ML
changeset 1786 8a31d85d27b8
parent 1777 47c47b7d7aa8
child 1817 3994d37b16ae
     1.1 --- a/src/HOL/Nat.ML	Mon Jun 03 11:44:44 1996 +0200
     1.2 +++ b/src/HOL/Nat.ML	Mon Jun 03 17:10:56 1996 +0200
     1.3 @@ -557,7 +557,7 @@
     1.4  	cut_facts_tac prems 1,
     1.5  	rtac select_equality 1,
     1.6  	fold_goals_tac [Least_def],
     1.7 -	safe_tac (HOL_cs addSEs [LeastI]),
     1.8 +	safe_tac (!claset addSEs [LeastI]),
     1.9  	res_inst_tac [("n","j")] natE 1,
    1.10  	Fast_tac 1,
    1.11  	fast_tac (!claset addDs [Suc_less_SucD] addDs [not_less_Least]) 1,	
    1.12 @@ -566,11 +566,11 @@
    1.13  	hyp_subst_tac 1,
    1.14  	rewtac Least_def,
    1.15  	rtac (select_equality RS arg_cong RS sym) 1,
    1.16 -	safe_tac HOL_cs,
    1.17 +	safe_tac (!claset),
    1.18  	dtac Suc_mono 1,
    1.19  	Fast_tac 1,
    1.20  	cut_facts_tac [less_linear] 1,
    1.21 -	safe_tac HOL_cs,
    1.22 +	safe_tac (!claset),
    1.23  	atac 2,
    1.24  	Fast_tac 2,
    1.25  	dtac Suc_mono 1,