src/HOL/Nat.ML
changeset 2031 03a843f0f447
parent 2009 9023e474d22a
child 2081 c2da3ca231ab
     1.1 --- a/src/HOL/Nat.ML	Thu Sep 26 11:11:22 1996 +0200
     1.2 +++ b/src/HOL/Nat.ML	Thu Sep 26 12:47:47 1996 +0200
     1.3 @@ -16,12 +16,12 @@
     1.4  
     1.5  (* Zero is a natural number -- this also justifies the type definition*)
     1.6  goal Nat.thy "Zero_Rep: Nat";
     1.7 -by (rtac (Nat_unfold RS ssubst) 1);
     1.8 +by (stac Nat_unfold 1);
     1.9  by (rtac (singletonI RS UnI1) 1);
    1.10  qed "Zero_RepI";
    1.11  
    1.12  val prems = goal Nat.thy "i: Nat ==> Suc_Rep(i) : Nat";
    1.13 -by (rtac (Nat_unfold RS ssubst) 1);
    1.14 +by (stac Nat_unfold 1);
    1.15  by (rtac (imageI RS UnI2) 1);
    1.16  by (resolve_tac prems 1);
    1.17  qed "Suc_RepI";
    1.18 @@ -293,12 +293,12 @@
    1.19  Addsimps [gr_implies_not0];
    1.20  
    1.21  qed_goal "zero_less_eq" Nat.thy "0 < n = (n ~= 0)" (fn _ => [
    1.22 -	rtac iffI 1,
    1.23 -	etac gr_implies_not0 1,
    1.24 -	rtac natE 1,
    1.25 -	contr_tac 1,
    1.26 -	etac ssubst 1,
    1.27 -	rtac zero_less_Suc 1]);
    1.28 +        rtac iffI 1,
    1.29 +        etac gr_implies_not0 1,
    1.30 +        rtac natE 1,
    1.31 +        contr_tac 1,
    1.32 +        etac ssubst 1,
    1.33 +        rtac zero_less_Suc 1]);
    1.34  
    1.35  (** Inductive (?) properties **)
    1.36  
    1.37 @@ -408,8 +408,8 @@
    1.38  
    1.39  (*
    1.40  goal Nat.thy "(Suc m < n | Suc m = n) = (m < n)";
    1.41 -by(stac (less_Suc_eq RS sym) 1);
    1.42 -by(rtac Suc_less_eq 1);
    1.43 +by (stac (less_Suc_eq RS sym) 1);
    1.44 +by (rtac Suc_less_eq 1);
    1.45  qed "Suc_le_eq";
    1.46  
    1.47  this could make the simpset (with less_Suc_eq added again) more confluent,
    1.48 @@ -562,23 +562,23 @@
    1.49  qed_goalw "Least_Suc" Nat.thy [Least_def]
    1.50   "!!P. [| ? n. P(Suc n); ~ P 0 |] ==> (LEAST n. P n) = Suc (LEAST m. P(Suc m))"
    1.51   (fn _ => [
    1.52 -	rtac select_equality 1,
    1.53 -	fold_goals_tac [Least_def],
    1.54 -	safe_tac (!claset addSEs [LeastI]),
    1.55 -	res_inst_tac [("n","j")] natE 1,
    1.56 -	Fast_tac 1,
    1.57 -	fast_tac (!claset addDs [Suc_less_SucD, not_less_Least]) 1,
    1.58 -	res_inst_tac [("n","k")] natE 1,
    1.59 -	Fast_tac 1,
    1.60 -	hyp_subst_tac 1,
    1.61 -	rewtac Least_def,
    1.62 -	rtac (select_equality RS arg_cong RS sym) 1,
    1.63 -	safe_tac (!claset),
    1.64 -	dtac Suc_mono 1,
    1.65 -	Fast_tac 1,
    1.66 -	cut_facts_tac [less_linear] 1,
    1.67 -	safe_tac (!claset),
    1.68 -	atac 2,
    1.69 -	Fast_tac 2,
    1.70 -	dtac Suc_mono 1,
    1.71 -	Fast_tac 1]);
    1.72 +        rtac select_equality 1,
    1.73 +        fold_goals_tac [Least_def],
    1.74 +        safe_tac (!claset addSEs [LeastI]),
    1.75 +        res_inst_tac [("n","j")] natE 1,
    1.76 +        Fast_tac 1,
    1.77 +        fast_tac (!claset addDs [Suc_less_SucD, not_less_Least]) 1,
    1.78 +        res_inst_tac [("n","k")] natE 1,
    1.79 +        Fast_tac 1,
    1.80 +        hyp_subst_tac 1,
    1.81 +        rewtac Least_def,
    1.82 +        rtac (select_equality RS arg_cong RS sym) 1,
    1.83 +        safe_tac (!claset),
    1.84 +        dtac Suc_mono 1,
    1.85 +        Fast_tac 1,
    1.86 +        cut_facts_tac [less_linear] 1,
    1.87 +        safe_tac (!claset),
    1.88 +        atac 2,
    1.89 +        Fast_tac 2,
    1.90 +        dtac Suc_mono 1,
    1.91 +        Fast_tac 1]);