1.1 --- a/src/HOL/Library/Nat_Infinity.thy	Wed Oct 03 20:54:05 2001 +0200
     1.2 +++ b/src/HOL/Library/Nat_Infinity.thy	Wed Oct 03 20:54:16 2001 +0200
     1.3 @@ -95,7 +95,7 @@
     1.4  lemma Fin_iless_Infty [simp]: "Fin n < \<infinity>"
     1.5    by (simp add: inat_defs split:inat_splits, arith?)
     1.6  
     1.7 -lemma Infty_eq [simp]: "n < \<infinity> = (n \<noteq> \<infinity>)"
     1.8 +lemma Infty_eq [simp]: "(n < \<infinity>) = (n \<noteq> \<infinity>)"
     1.9    by (simp add: inat_defs split:inat_splits, arith?)
    1.10  
    1.11  lemma i0_eq [simp]: "((0::inat) < n) = (n \<noteq> 0)"
    1.12 @@ -110,13 +110,13 @@
    1.13  lemma Fin_iless: "n < Fin m ==> \<exists>k. n = Fin k"
    1.14    by (simp add: inat_defs split:inat_splits, arith?)
    1.15  
    1.16 -lemma iSuc_mono [simp]: "iSuc n < iSuc m = (n < m)"
    1.17 +lemma iSuc_mono [simp]: "(iSuc n < iSuc m) = (n < m)"
    1.18    by (simp add: inat_defs split:inat_splits, arith?)
    1.19  
    1.20  
    1.21  (* ----------------------------------------------------------------------- *)
    1.22  
    1.23 -lemma ile_def2: "m \<le> n = (m < n \<or> m = (n::inat))"
    1.24 +lemma ile_def2: "(m \<le> n) = (m < n \<or> m = (n::inat))"
    1.25    by (simp add: inat_defs split:inat_splits, arith?)
    1.26  
    1.27  lemma ile_refl [simp]: "n \<le> (n::inat)"
    1.28 @@ -149,13 +149,13 @@
    1.29  lemma ileI1: "m < n ==> iSuc m \<le> n"
    1.30    by (simp add: inat_defs split:inat_splits, arith?)
    1.31  
    1.32 -lemma Suc_ile_eq: "Fin (Suc m) \<le> n = (Fin m < n)"
    1.33 +lemma Suc_ile_eq: "(Fin (Suc m) \<le> n) = (Fin m < n)"
    1.34    by (simp add: inat_defs split:inat_splits, arith?)
    1.35  
    1.36 -lemma iSuc_ile_mono [simp]: "iSuc n \<le> iSuc m = (n \<le> m)"
    1.37 +lemma iSuc_ile_mono [simp]: "(iSuc n \<le> iSuc m) = (n \<le> m)"
    1.38    by (simp add: inat_defs split:inat_splits, arith?)
    1.39  
    1.40 -lemma iless_Suc_eq [simp]: "Fin m < iSuc n = (Fin m \<le> n)"
    1.41 +lemma iless_Suc_eq [simp]: "(Fin m < iSuc n) = (Fin m \<le> n)"
    1.42    by (simp add: inat_defs split:inat_splits, arith?)
    1.43  
    1.44  lemma not_iSuc_ilei0 [simp]: "\<not> iSuc n \<le> 0"