src/HOL/Nat.ML
changeset 1465 5d7a7e439cec
parent 1327 6c29cfab679c
child 1475 7f5a4cd08209
     1.1 --- a/src/HOL/Nat.ML	Tue Jan 30 15:19:20 1996 +0100
     1.2 +++ b/src/HOL/Nat.ML	Tue Jan 30 15:24:36 1996 +0100
     1.3 @@ -1,6 +1,6 @@
     1.4 -(*  Title: 	HOL/nat
     1.5 +(*  Title:      HOL/nat
     1.6      ID:         $Id$
     1.7 -    Author: 	Tobias Nipkow, Cambridge University Computer Laboratory
     1.8 +    Author:     Tobias Nipkow, Cambridge University Computer Laboratory
     1.9      Copyright   1991  University of Cambridge
    1.10  
    1.11  For nat.thy.  Type nat is defined as a set (Nat) over the type ind.
    1.12 @@ -47,7 +47,7 @@
    1.13  (*Perform induction on n. *)
    1.14  fun nat_ind_tac a i = 
    1.15      EVERY [res_inst_tac [("n",a)] nat_induct i,
    1.16 -	   rename_last_tac a ["1"] (i+1)];
    1.17 +           rename_last_tac a ["1"] (i+1)];
    1.18  
    1.19  (*A special form of induction for reasoning about m<n and m-n*)
    1.20  val prems = goal Nat.thy
    1.21 @@ -133,7 +133,7 @@
    1.22  
    1.23  goalw Nat.thy [nat_case_def] "nat_case a f (Suc k) = f(k)";
    1.24  by (fast_tac (set_cs addIs [select_equality] 
    1.25 -	               addEs [make_elim Suc_inject, Suc_neq_Zero]) 1);
    1.26 +                       addEs [make_elim Suc_inject, Suc_neq_Zero]) 1);
    1.27  qed "nat_case_Suc";
    1.28  
    1.29  (** Introduction rules for 'pred_nat' **)
    1.30 @@ -153,7 +153,7 @@
    1.31  by (strip_tac 1);
    1.32  by (nat_ind_tac "x" 1);
    1.33  by (fast_tac (HOL_cs addSEs [mp, pred_natE, Pair_inject, 
    1.34 -			     make_elim Suc_inject]) 2);
    1.35 +                             make_elim Suc_inject]) 2);
    1.36  by (fast_tac (HOL_cs addSEs [mp, pred_natE, Pair_inject, Zero_neq_Suc]) 1);
    1.37  qed "wf_pred_nat";
    1.38  
    1.39 @@ -245,7 +245,7 @@
    1.40  \    |] ==> P";
    1.41  by (rtac (major RS tranclE) 1);
    1.42  by (REPEAT_FIRST (bound_hyp_subst_tac ORELSE'
    1.43 -		  eresolve_tac (prems@[pred_natE, Pair_inject])));
    1.44 +                  eresolve_tac (prems@[pred_natE, Pair_inject])));
    1.45  by (rtac refl 1);
    1.46  qed "lessE";
    1.47  
    1.48 @@ -271,7 +271,7 @@
    1.49  
    1.50  goal Nat.thy "(m < Suc(n)) = (m < n | m = n)";
    1.51  by (fast_tac (HOL_cs addSIs [lessI]
    1.52 -		     addEs  [less_trans, less_SucE]) 1);
    1.53 +                     addEs  [less_trans, less_SucE]) 1);
    1.54  qed "less_Suc_eq";
    1.55  
    1.56  val prems = goal Nat.thy "m<n ==> n ~= 0";
    1.57 @@ -289,8 +289,8 @@
    1.58  by (rtac impI 1);
    1.59  by (etac less_zeroE 1);
    1.60  by (fast_tac (HOL_cs addSIs [lessI RS less_SucI]
    1.61 -	 	     addSDs [Suc_inject]
    1.62 -		     addEs  [less_trans, lessE]) 1);
    1.63 +                     addSDs [Suc_inject]
    1.64 +                     addEs  [less_trans, lessE]) 1);
    1.65  qed "Suc_lessD";
    1.66  
    1.67  val [major,minor] = goal Nat.thy 
    1.68 @@ -315,8 +315,8 @@
    1.69  by (rtac impI 1);
    1.70  by (etac less_zeroE 1);
    1.71  by (fast_tac (HOL_cs addSIs [lessI]
    1.72 -	 	     addSDs [Suc_inject]
    1.73 -		     addEs  [less_trans, lessE]) 1);
    1.74 +                     addSDs [Suc_inject]
    1.75 +                     addEs  [less_trans, lessE]) 1);
    1.76  qed "Suc_mono";
    1.77  
    1.78  goal Nat.thy "(Suc(m) < Suc(n)) = (m<n)";