src/HOL/Nat.ML
changeset 972 e61b058d58d2
parent 962 136308504cd9
child 1024 b86042000035
     1.1 --- a/src/HOL/Nat.ML	Thu Mar 23 15:39:13 1995 +0100
     1.2 +++ b/src/HOL/Nat.ML	Fri Mar 24 12:30:35 1995 +0100
     1.3 @@ -136,12 +136,12 @@
     1.4  
     1.5  (** Introduction rules for 'pred_nat' **)
     1.6  
     1.7 -goalw Nat.thy [pred_nat_def] "<n, Suc(n)> : pred_nat";
     1.8 +goalw Nat.thy [pred_nat_def] "(n, Suc(n)) : pred_nat";
     1.9  by (fast_tac set_cs 1);
    1.10  qed "pred_natI";
    1.11  
    1.12  val major::prems = goalw Nat.thy [pred_nat_def]
    1.13 -    "[| p : pred_nat;  !!x n. [| p = <n, Suc(n)> |] ==> R \
    1.14 +    "[| p : pred_nat;  !!x n. [| p = (n, Suc(n)) |] ==> R \
    1.15  \    |] ==> R";
    1.16  by (rtac (major RS CollectE) 1);
    1.17  by (REPEAT (eresolve_tac ([asm_rl,exE]@prems) 1));
    1.18 @@ -204,7 +204,7 @@
    1.19  by (rtac (pred_natI RS r_into_trancl) 1);
    1.20  qed "lessI";
    1.21  
    1.22 -(* i<j ==> i<Suc(j) *)
    1.23 +(* i(j ==> i(Suc(j) *)
    1.24  val less_SucI = lessI RSN (2, less_trans);
    1.25  
    1.26  goal Nat.thy "0 < Suc(n)";
    1.27 @@ -220,7 +220,7 @@
    1.28  by(fast_tac (HOL_cs addIs ([wf_pred_nat, wf_trancl RS wf_asym]@prems))1);
    1.29  qed "less_not_sym";
    1.30  
    1.31 -(* [| n<m; m<n |] ==> R *)
    1.32 +(* [| n(m; m(n |] ==> R *)
    1.33  bind_thm ("less_asym", (less_not_sym RS notE));
    1.34  
    1.35  goalw Nat.thy [less_def] "~ n<(n::nat)";
    1.36 @@ -228,7 +228,7 @@
    1.37  by (etac (wf_pred_nat RS wf_trancl RS wf_anti_refl) 1);
    1.38  qed "less_not_refl";
    1.39  
    1.40 -(* n<n ==> R *)
    1.41 +(* n(n ==> R *)
    1.42  bind_thm ("less_anti_refl", (less_not_refl RS notE));
    1.43  
    1.44  goal Nat.thy "!!m. n<m ==> m ~= (n::nat)";