# HG changeset patch
# User nipkow
# Date 1089889894 -7200
# Node ID d59f7e2e18d3ef81128b428a721fba05a258e0fd
# Parent  f224d27bb1f8caff9d8ec2d057dce52870b0c5d8
Moved to new m<..<n syntax for set intervals.

diff -r f224d27bb1f8 -r d59f7e2e18d3 src/HOL/Algebra/UnivPoly.thy
--- a/src/HOL/Algebra/UnivPoly.thy	Thu Jul 15 08:38:37 2004 +0200
+++ b/src/HOL/Algebra/UnivPoly.thy	Thu Jul 15 13:11:34 2004 +0200
@@ -646,13 +646,13 @@
         "!!i. [| n < i; i <= n + m |] ==> n + m - i < m" by arith
       from True have "coeff P (monom P \<one> (Suc n)) k = \<one>" by simp
       also from True
-      have "... = (\<Oplus>i \<in> {..n(} \<union> {n}. coeff P (monom P \<one> n) i \<otimes>
+      have "... = (\<Oplus>i \<in> {..<n} \<union> {n}. coeff P (monom P \<one> n) i \<otimes>
         coeff P (monom P \<one> 1) (k - i))"
         by (simp cong: finsum_cong add: finsum_Un_disjoint Pi_def)
       also have "... = (\<Oplus>i \<in>  {..n}. coeff P (monom P \<one> n) i \<otimes>
         coeff P (monom P \<one> 1) (k - i))"
         by (simp only: ivl_disj_un_singleton)
-      also from True have "... = (\<Oplus>i \<in> {..n} \<union> {)n..k}. coeff P (monom P \<one> n) i \<otimes>
+      also from True have "... = (\<Oplus>i \<in> {..n} \<union> {n<..k}. coeff P (monom P \<one> n) i \<otimes>
         coeff P (monom P \<one> 1) (k - i))"
         by (simp cong: finsum_cong add: finsum_Un_disjoint ivl_disj_int_one
           order_less_imp_not_eq Pi_def)
@@ -668,10 +668,10 @@
     from neq have "coeff P (monom P \<one> (Suc n)) k = \<zero>" by simp
     also have "... = (\<Oplus>i \<in> {..k}. ?s i)"
     proof -
-      have f1: "(\<Oplus>i \<in> {..n(}. ?s i) = \<zero>" by (simp cong: finsum_cong add: Pi_def)
+      have f1: "(\<Oplus>i \<in> {..<n}. ?s i) = \<zero>" by (simp cong: finsum_cong add: Pi_def)
       from neq have f2: "(\<Oplus>i \<in> {n}. ?s i) = \<zero>"
         by (simp cong: finsum_cong add: Pi_def) arith
-      have f3: "n < k ==> (\<Oplus>i \<in> {)n..k}. ?s i) = \<zero>"
+      have f3: "n < k ==> (\<Oplus>i \<in> {n<..k}. ?s i) = \<zero>"
         by (simp cong: finsum_cong add: order_less_imp_not_eq Pi_def)
       show ?thesis
       proof (cases "k < n")
@@ -681,7 +681,7 @@
         show ?thesis
         proof (cases "n = k")
           case True
-          then have "\<zero> = (\<Oplus>i \<in> {..n(} \<union> {n}. ?s i)"
+          then have "\<zero> = (\<Oplus>i \<in> {..<n} \<union> {n}. ?s i)"
             by (simp cong: finsum_cong add: finsum_Un_disjoint
               ivl_disj_int_singleton Pi_def)
           also from True have "... = (\<Oplus>i \<in> {..k}. ?s i)"
@@ -689,12 +689,12 @@
           finally show ?thesis .
         next
           case False with n_le_k have n_less_k: "n < k" by arith
-          with neq have "\<zero> = (\<Oplus>i \<in> {..n(} \<union> {n}. ?s i)"
+          with neq have "\<zero> = (\<Oplus>i \<in> {..<n} \<union> {n}. ?s i)"
             by (simp add: finsum_Un_disjoint f1 f2
               ivl_disj_int_singleton Pi_def del: Un_insert_right)
           also have "... = (\<Oplus>i \<in> {..n}. ?s i)"
             by (simp only: ivl_disj_un_singleton)
-          also from n_less_k neq have "... = (\<Oplus>i \<in> {..n} \<union> {)n..k}. ?s i)"
+          also from n_less_k neq have "... = (\<Oplus>i \<in> {..n} \<union> {n<..k}. ?s i)"
             by (simp add: finsum_Un_disjoint f3 ivl_disj_int_one Pi_def)
           also from n_less_k have "... = (\<Oplus>i \<in> {..k}. ?s i)"
             by (simp only: ivl_disj_un_one)
@@ -976,12 +976,12 @@
   show "deg R p + deg R q <= deg R (p \<otimes>\<^sub>2 q)"
   proof (rule deg_belowI, simp add: R)
     have "finsum R ?s {.. deg R p + deg R q}
-      = finsum R ?s ({.. deg R p(} Un {deg R p .. deg R p + deg R q})"
+      = finsum R ?s ({..< deg R p} Un {deg R p .. deg R p + deg R q})"
       by (simp only: ivl_disj_un_one)
     also have "... = finsum R ?s {deg R p .. deg R p + deg R q}"
       by (simp cong: finsum_cong add: finsum_Un_disjoint ivl_disj_int_one
         deg_aboveD less_add_diff R Pi_def)
-    also have "...= finsum R ?s ({deg R p} Un {)deg R p .. deg R p + deg R q})"
+    also have "...= finsum R ?s ({deg R p} Un {deg R p <.. deg R p + deg R q})"
       by (simp only: ivl_disj_un_singleton)
     also have "... = coeff P p (deg R p) \<otimes> coeff P q (deg R q)"
       by (simp cong: finsum_cong add: finsum_Un_disjoint
@@ -1015,14 +1015,14 @@
   proof (cases "k <= deg R p")
     case True
     hence "coeff P (finsum P ?s {..deg R p}) k =
-          coeff P (finsum P ?s ({..k} Un {)k..deg R p})) k"
+          coeff P (finsum P ?s ({..k} Un {k<..deg R p})) k"
       by (simp only: ivl_disj_un_one)
     also from True
     have "... = coeff P (finsum P ?s {..k}) k"
       by (simp cong: finsum_cong add: finsum_Un_disjoint
         ivl_disj_int_one order_less_imp_not_eq2 coeff_finsum R RR Pi_def)
     also
-    have "... = coeff P (finsum P ?s ({..k(} Un {k})) k"
+    have "... = coeff P (finsum P ?s ({..<k} Un {k})) k"
       by (simp only: ivl_disj_un_singleton)
     also have "... = coeff P p k"
       by (simp cong: finsum_cong add: setsum_Un_disjoint
@@ -1031,7 +1031,7 @@
   next
     case False
     hence "coeff P (finsum P ?s {..deg R p}) k =
-          coeff P (finsum P ?s ({..deg R p(} Un {deg R p})) k"
+          coeff P (finsum P ?s ({..<deg R p} Un {deg R p})) k"
       by (simp only: ivl_disj_un_singleton)
     also from False have "... = coeff P p k"
       by (simp cong: finsum_cong add: setsum_Un_disjoint ivl_disj_int_singleton
@@ -1046,7 +1046,7 @@
 proof -
   let ?s = "(%i. monom P (coeff P p i) i)"
   assume R: "p \<in> carrier P" and "deg R p <= n"
-  then have "finsum P ?s {..n} = finsum P ?s ({..deg R p} Un {)deg R p..n})"
+  then have "finsum P ?s {..n} = finsum P ?s ({..deg R p} Un {deg R p<..n})"
     by (simp only: ivl_disj_un_one)
   also have "... = finsum P ?s {..deg R p}"
     by (simp cong: UP_finsum_cong add: UP_finsum_Un_disjoint ivl_disj_int_one
@@ -1206,12 +1206,12 @@
   from f g have "(\<Oplus>k \<in> {..n + m}. \<Oplus>i \<in> {..k}. f i \<otimes> g (k - i)) =
       (\<Oplus>k \<in> {..n + m}. \<Oplus>i \<in> {..n + m - k}. f k \<otimes> g i)"
     by (simp add: diagonal_sum Pi_def)
-  also have "... = (\<Oplus>k \<in> {..n} \<union> {)n..n + m}. \<Oplus>i \<in> {..n + m - k}. f k \<otimes> g i)"
+  also have "... = (\<Oplus>k \<in> {..n} \<union> {n<..n + m}. \<Oplus>i \<in> {..n + m - k}. f k \<otimes> g i)"
     by (simp only: ivl_disj_un_one)
   also from f g have "... = (\<Oplus>k \<in> {..n}. \<Oplus>i \<in> {..n + m - k}. f k \<otimes> g i)"
     by (simp cong: finsum_cong
       add: bound.bound [OF bf] finsum_Un_disjoint ivl_disj_int_one Pi_def)
-  also from f g have "... = (\<Oplus>k \<in> {..n}. \<Oplus>i \<in> {..m} \<union> {)m..n + m - k}. f k \<otimes> g i)"
+  also from f g have "... = (\<Oplus>k \<in> {..n}. \<Oplus>i \<in> {..m} \<union> {m<..n + m - k}. f k \<otimes> g i)"
     by (simp cong: finsum_cong add: ivl_disj_un_one le_add_diff Pi_def)
   also from f g have "... = (\<Oplus>k \<in> {..n}. \<Oplus>i \<in> {..m}. f k \<otimes> g i)"
     by (simp cong: finsum_cong
@@ -1262,7 +1262,7 @@
   proof (simp only: eval_on_carrier UP_mult_closed)
     from RS have
       "(\<Oplus>\<^sub>2 i \<in> {..deg R (p \<otimes>\<^sub>3 q)}. h (coeff P (p \<otimes>\<^sub>3 q) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) =
-      (\<Oplus>\<^sub>2 i \<in> {..deg R (p \<otimes>\<^sub>3 q)} \<union> {)deg R (p \<otimes>\<^sub>3 q)..deg R p + deg R q}.
+      (\<Oplus>\<^sub>2 i \<in> {..deg R (p \<otimes>\<^sub>3 q)} \<union> {deg R (p \<otimes>\<^sub>3 q)<..deg R p + deg R q}.
         h (coeff P (p \<otimes>\<^sub>3 q) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i)"
       by (simp cong: finsum_cong
         add: deg_aboveD finsum_Un_disjoint ivl_disj_int_one Pi_def
@@ -1292,7 +1292,7 @@
   proof (simp only: eval_on_carrier UP_a_closed)
     from RS have
       "(\<Oplus>\<^sub>2i \<in> {..deg R (p \<oplus>\<^sub>3 q)}. h (coeff P (p \<oplus>\<^sub>3 q) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) =
-      (\<Oplus>\<^sub>2i \<in> {..deg R (p \<oplus>\<^sub>3 q)} \<union> {)deg R (p \<oplus>\<^sub>3 q)..max (deg R p) (deg R q)}.
+      (\<Oplus>\<^sub>2i \<in> {..deg R (p \<oplus>\<^sub>3 q)} \<union> {deg R (p \<oplus>\<^sub>3 q)<..max (deg R p) (deg R q)}.
         h (coeff P (p \<oplus>\<^sub>3 q) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i)"
       by (simp cong: finsum_cong
         add: deg_aboveD finsum_Un_disjoint ivl_disj_int_one Pi_def
@@ -1306,9 +1306,9 @@
       by (simp cong: finsum_cong
         add: l_distr deg_aboveD finsum_Un_disjoint ivl_disj_int_one Pi_def)
     also have "... =
-        (\<Oplus>\<^sub>2 i \<in> {..deg R p} \<union> {)deg R p..max (deg R p) (deg R q)}.
+        (\<Oplus>\<^sub>2 i \<in> {..deg R p} \<union> {deg R p<..max (deg R p) (deg R q)}.
           h (coeff P p i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) \<oplus>\<^sub>2
-        (\<Oplus>\<^sub>2 i \<in> {..deg R q} \<union> {)deg R q..max (deg R p) (deg R q)}.
+        (\<Oplus>\<^sub>2 i \<in> {..deg R q} \<union> {deg R q<..max (deg R p) (deg R q)}.
           h (coeff P q i) \<otimes>\<^sub>2 s (^)\<^sub>2 i)"
       by (simp only: ivl_disj_un_one le_maxI1 le_maxI2)
     also from RS have "... =
@@ -1392,7 +1392,7 @@
   assume S: "s \<in> carrier S"
   then have
     "(\<Oplus>\<^sub>2 i \<in> {..deg R (monom P \<one> 1)}. h (coeff P (monom P \<one> 1) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) =
-    (\<Oplus>\<^sub>2i\<in>{..deg R (monom P \<one> 1)} \<union> {)deg R (monom P \<one> 1)..1}.
+    (\<Oplus>\<^sub>2i\<in>{..deg R (monom P \<one> 1)} \<union> {deg R (monom P \<one> 1)<..1}.
       h (coeff P (monom P \<one> 1) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i)"
     by (simp cong: finsum_cong del: coeff_monom
       add: deg_aboveD finsum_Un_disjoint ivl_disj_int_one Pi_def)
diff -r f224d27bb1f8 -r d59f7e2e18d3 src/HOL/Algebra/poly/UnivPoly2.thy
--- a/src/HOL/Algebra/poly/UnivPoly2.thy	Thu Jul 15 08:38:37 2004 +0200
+++ b/src/HOL/Algebra/poly/UnivPoly2.thy	Thu Jul 15 13:11:34 2004 +0200
@@ -643,12 +643,12 @@
   show "deg p + deg q <= deg (p * q)"
   proof (rule deg_belowI, simp)
     have "setsum ?s {.. deg p + deg q}
-      = setsum ?s ({.. deg p(} Un {deg p .. deg p + deg q})"
+      = setsum ?s ({..< deg p} Un {deg p .. deg p + deg q})"
       by (simp only: ivl_disj_un_one)
     also have "... = setsum ?s {deg p .. deg p + deg q}"
       by (simp add: setsum_Un_disjoint ivl_disj_int_one
         setsum_0 deg_aboveD less_add_diff)
-    also have "... = setsum ?s ({deg p} Un {)deg p .. deg p + deg q})"
+    also have "... = setsum ?s ({deg p} Un {deg p <.. deg p + deg q})"
       by (simp only: ivl_disj_un_singleton)
     also have "... = coeff p (deg p) * coeff q (deg q)" 
       by (simp add: setsum_Un_disjoint ivl_disj_int_singleton 
@@ -686,14 +686,14 @@
   proof (cases "k <= deg p")
     case True
     hence "coeff (setsum ?s {..deg p}) k = 
-          coeff (setsum ?s ({..k} Un {)k..deg p})) k"
+          coeff (setsum ?s ({..k} Un {k<..deg p})) k"
       by (simp only: ivl_disj_un_one)
     also from True
     have "... = coeff (setsum ?s {..k}) k"
       by (simp add: setsum_Un_disjoint ivl_disj_int_one order_less_imp_not_eq2
         setsum_0 coeff_natsum )
     also
-    have "... = coeff (setsum ?s ({..k(} Un {k})) k"
+    have "... = coeff (setsum ?s ({..<k} Un {k})) k"
       by (simp only: ivl_disj_un_singleton)
     also have "... = coeff p k"
       by (simp add: setsum_Un_disjoint ivl_disj_int_singleton 
@@ -702,7 +702,7 @@
   next
     case False
     hence "coeff (setsum ?s {..deg p}) k = 
-          coeff (setsum ?s ({..deg p(} Un {deg p})) k"
+          coeff (setsum ?s ({..<deg p} Un {deg p})) k"
       by (simp only: ivl_disj_un_singleton)
     also from False have "... = coeff p k"
       by (simp add: setsum_Un_disjoint ivl_disj_int_singleton 
@@ -716,7 +716,7 @@
 proof -
   let ?s = "(%i. monom (coeff p i) i)"
   assume "deg p <= n"
-  then have "setsum ?s {..n} = setsum ?s ({..deg p} Un {)deg p..n})"
+  then have "setsum ?s {..n} = setsum ?s ({..deg p} Un {deg p<..n})"
     by (simp only: ivl_disj_un_one)
   also have "... = setsum ?s {..deg p}"
     by (simp add: setsum_Un_disjoint ivl_disj_int_one
diff -r f224d27bb1f8 -r d59f7e2e18d3 src/HOL/HoareParallel/OG_Examples.thy
--- a/src/HOL/HoareParallel/OG_Examples.thy	Thu Jul 15 08:38:37 2004 +0200
+++ b/src/HOL/HoareParallel/OG_Examples.thy	Thu Jul 15 13:11:34 2004 +0200
@@ -513,10 +513,10 @@
 lemma Example2_lemma2: 
  "!!b. \<lbrakk>j<n; b j=0\<rbrakk> \<Longrightarrow> Suc (\<Sum>i::nat< n. b i)=(\<Sum>i< n. (b (j := Suc 0)) i)"
 apply(frule_tac b="(b (j:=(Suc 0)))" in Example2_lemma2_aux)
-apply(erule_tac  t="setsum (b(j := (Suc 0))) {..n(}" in ssubst)
+apply(erule_tac  t="setsum (b(j := (Suc 0))) {..<n}" in ssubst)
 apply(frule_tac b=b in Example2_lemma2_aux)
-apply(erule_tac  t="setsum b {..n(}" in ssubst)
-apply(subgoal_tac "Suc (setsum b {..j(} + b j + (\<Sum>i<n - Suc j. b (Suc j + i)))=(setsum b {..j(} + Suc (b j) + (\<Sum>i<n - Suc j. b (Suc j + i)))")
+apply(erule_tac  t="setsum b {..<n}" in ssubst)
+apply(subgoal_tac "Suc (setsum b {..<j} + b j + (\<Sum>i<n - Suc j. b (Suc j + i)))=(setsum b {..<j} + Suc (b j) + (\<Sum>i<n - Suc j. b (Suc j + i)))")
 apply(rotate_tac -1)
 apply(erule ssubst)
 apply(subgoal_tac "j\<le>j")
diff -r f224d27bb1f8 -r d59f7e2e18d3 src/HOL/HoareParallel/RG_Examples.thy
--- a/src/HOL/HoareParallel/RG_Examples.thy	Thu Jul 15 08:38:37 2004 +0200
+++ b/src/HOL/HoareParallel/RG_Examples.thy	Thu Jul 15 13:11:34 2004 +0200
@@ -212,10 +212,10 @@
 lemma Example2_lemma2: 
  "!!b. \<lbrakk>j<n; b j=0\<rbrakk> \<Longrightarrow> Suc (\<Sum>i::nat< n. b i)=(\<Sum>i< n. (b (j := Suc 0)) i)"
 apply(frule_tac b="(b (j:=(Suc 0)))" in Example2_lemma2_aux)
-apply(erule_tac  t="setsum (b(j := (Suc 0))) {..n(}" in ssubst)
+apply(erule_tac  t="setsum (b(j := (Suc 0))) {..<n}" in ssubst)
 apply(frule_tac b=b in Example2_lemma2_aux)
-apply(erule_tac  t="setsum b {..n(}" in ssubst)
-apply(subgoal_tac "Suc (setsum b {..j(} + b j + (\<Sum>i<n - Suc j. b (Suc j + i)))=(setsum b {..j(} + Suc (b j) + (\<Sum>i<n - Suc j. b (Suc j + i)))")
+apply(erule_tac  t="setsum b {..<n}" in ssubst)
+apply(subgoal_tac "Suc (setsum b {..<j} + b j + (\<Sum>i<n - Suc j. b (Suc j + i)))=(setsum b {..<j} + Suc (b j) + (\<Sum>i<n - Suc j. b (Suc j + i)))")
 apply(rotate_tac -1)
 apply(erule ssubst)
 apply(subgoal_tac "j\<le>j")
diff -r f224d27bb1f8 -r d59f7e2e18d3 src/HOL/Infinite_Set.thy
--- a/src/HOL/Infinite_Set.thy	Thu Jul 15 08:38:37 2004 +0200
+++ b/src/HOL/Infinite_Set.thy	Thu Jul 15 13:11:34 2004 +0200
@@ -68,7 +68,7 @@
 
 lemma finite_nat_bounded:
   assumes S: "finite (S::nat set)"
-  shows "\<exists>k. S \<subseteq> {..k(}" (is "\<exists>k. ?bounded S k")
+  shows "\<exists>k. S \<subseteq> {..<k}" (is "\<exists>k. ?bounded S k")
 using S
 proof (induct)
   have "?bounded {} 0" by simp
@@ -89,13 +89,13 @@
 qed
 
 lemma finite_nat_iff_bounded:
-  "finite (S::nat set) = (\<exists>k. S \<subseteq> {..k(})" (is "?lhs = ?rhs")
+  "finite (S::nat set) = (\<exists>k. S \<subseteq> {..<k})" (is "?lhs = ?rhs")
 proof
   assume ?lhs
   thus ?rhs by (rule finite_nat_bounded)
 next
   assume ?rhs
-  then obtain k where "S \<subseteq> {..k(}" ..
+  then obtain k where "S \<subseteq> {..<k}" ..
   thus "finite S"
     by (rule finite_subset, simp)
 qed
@@ -104,7 +104,7 @@
   "finite (S::nat set) = (\<exists>k. S \<subseteq> {..k})" (is "?lhs = ?rhs")
 proof
   assume ?lhs
-  then obtain k where "S \<subseteq> {..k(}" 
+  then obtain k where "S \<subseteq> {..<k}" 
     by (blast dest: finite_nat_bounded)
   hence "S \<subseteq> {..k}" by auto
   thus ?rhs ..
diff -r f224d27bb1f8 -r d59f7e2e18d3 src/HOL/List.thy
--- a/src/HOL/List.thy	Thu Jul 15 08:38:37 2004 +0200
+++ b/src/HOL/List.thy	Thu Jul 15 13:11:34 2004 +0200
@@ -1526,7 +1526,7 @@
 lemma sublist_singleton [simp]: "sublist [x] A = (if 0 : A then [x] else [])"
 by (simp add: sublist_Cons)
 
-lemma sublist_upt_eq_take [simp]: "sublist l {..n(} = take n l"
+lemma sublist_upt_eq_take [simp]: "sublist l {..<n} = take n l"
 apply (induct l rule: rev_induct, simp)
 apply (simp split: nat_diff_split add: sublist_append)
 done
diff -r f224d27bb1f8 -r d59f7e2e18d3 src/HOL/MicroJava/BV/BVExample.thy
--- a/src/HOL/MicroJava/BV/BVExample.thy	Thu Jul 15 08:38:37 2004 +0200
+++ b/src/HOL/MicroJava/BV/BVExample.thy	Thu Jul 15 13:11:34 2004 +0200
@@ -416,7 +416,7 @@
     in  kiljvm G mxs (1+size pTs+mxl) rT et instr start)"
 
 lemma [code]:
-  "unstables r step ss = (UN p:{..size ss(}. if \<not>stable r step ss p then {p} else {})"
+  "unstables r step ss = (UN p:{..<size ss}. if \<not>stable r step ss p then {p} else {})"
   apply (unfold unstables_def)
   apply (rule equalityI)
   apply (rule subsetI)
diff -r f224d27bb1f8 -r d59f7e2e18d3 src/HOL/SetInterval.thy
--- a/src/HOL/SetInterval.thy	Thu Jul 15 08:38:37 2004 +0200
+++ b/src/HOL/SetInterval.thy	Thu Jul 15 13:11:34 2004 +0200
@@ -12,30 +12,44 @@
 theory SetInterval = IntArith:
 
 constdefs
-  lessThan    :: "('a::ord) => 'a set"	("(1{.._'(})")
-  "{..u(} == {x. x<u}"
+  lessThan    :: "('a::ord) => 'a set"	("(1{..<_})")
+  "{..<u} == {x. x<u}"
 
   atMost      :: "('a::ord) => 'a set"	("(1{.._})")
   "{..u} == {x. x<=u}"
 
-  greaterThan :: "('a::ord) => 'a set"	("(1{')_..})")
-  "{)l..} == {x. l<x}"
+  greaterThan :: "('a::ord) => 'a set"	("(1{_<..})")
+  "{l<..} == {x. l<x}"
 
   atLeast     :: "('a::ord) => 'a set"	("(1{_..})")
   "{l..} == {x. l<=x}"
 
-  greaterThanLessThan :: "['a::ord, 'a] => 'a set"  ("(1{')_.._'(})")
-  "{)l..u(} == {)l..} Int {..u(}"
+  greaterThanLessThan :: "['a::ord, 'a] => 'a set"  ("(1{_<..<_})")
+  "{l<..<u} == {l<..} Int {..<u}"
 
-  atLeastLessThan :: "['a::ord, 'a] => 'a set"      ("(1{_.._'(})")
-  "{l..u(} == {l..} Int {..u(}"
+  atLeastLessThan :: "['a::ord, 'a] => 'a set"      ("(1{_..<_})")
+  "{l..<u} == {l..} Int {..<u}"
 
-  greaterThanAtMost :: "['a::ord, 'a] => 'a set"    ("(1{')_.._})")
-  "{)l..u} == {)l..} Int {..u}"
+  greaterThanAtMost :: "['a::ord, 'a] => 'a set"    ("(1{_<.._})")
+  "{l<..u} == {l<..} Int {..u}"
 
   atLeastAtMost :: "['a::ord, 'a] => 'a set"        ("(1{_.._})")
   "{l..u} == {l..} Int {..u}"
 
+(* Old syntax, will disappear! *)
+syntax
+  "_lessThan"    :: "('a::ord) => 'a set"	("(1{.._'(})")
+  "_greaterThan" :: "('a::ord) => 'a set"	("(1{')_..})")
+  "_greaterThanLessThan" :: "['a::ord, 'a] => 'a set"  ("(1{')_.._'(})")
+  "_atLeastLessThan" :: "['a::ord, 'a] => 'a set"      ("(1{_.._'(})")
+  "_greaterThanAtMost" :: "['a::ord, 'a] => 'a set"    ("(1{')_.._})")
+translations
+  "{..m(}" => "{..<m}"
+  "{)m..}" => "{m<..}"
+  "{)m..n(}" => "{m<..<n}"
+  "{m..n(}" => "{m..<n}"
+  "{)m..n}" => "{m<..n}"
+
 syntax
   "@UNION_le"   :: "nat => nat => 'b set => 'b set"       ("(3UN _<=_./ _)" 10)
   "@UNION_less" :: "nat => nat => 'b set => 'b set"       ("(3UN _<_./ _)" 10)
@@ -56,9 +70,9 @@
 
 translations
   "UN i<=n. A"  == "UN i:{..n}. A"
-  "UN i<n. A"   == "UN i:{..n(}. A"
+  "UN i<n. A"   == "UN i:{..<n}. A"
   "INT i<=n. A" == "INT i:{..n}. A"
-  "INT i<n. A"  == "INT i:{..n(}. A"
+  "INT i<n. A"  == "INT i:{..<n}. A"
 
 
 subsection {* Various equivalences *}
@@ -150,19 +164,19 @@
 text {* @{text greaterThanLessThan} *}
 
 lemma greaterThanLessThan_iff [simp]:
-  "(i : {)l..u(}) = (l < i & i < u)"
+  "(i : {l<..<u}) = (l < i & i < u)"
 by (simp add: greaterThanLessThan_def)
 
 text {* @{text atLeastLessThan} *}
 
 lemma atLeastLessThan_iff [simp]:
-  "(i : {l..u(}) = (l <= i & i < u)"
+  "(i : {l..<u}) = (l <= i & i < u)"
 by (simp add: atLeastLessThan_def)
 
 text {* @{text greaterThanAtMost} *}
 
 lemma greaterThanAtMost_iff [simp]:
-  "(i : {)l..u}) = (l < i & i <= u)"
+  "(i : {l<..u}) = (l < i & i <= u)"
 by (simp add: greaterThanAtMost_def)
 
 text {* @{text atLeastAtMost} *}
@@ -229,40 +243,40 @@
 lemma UN_atMost_UNIV: "(UN m::nat. atMost m) = UNIV"
 by blast
 
-lemma atLeast0LessThan [simp]: "{0::nat..n(} = {..n(}"
+lemma atLeast0LessThan [simp]: "{0::nat..<n} = {..<n}"
 by(simp add:lessThan_def atLeastLessThan_def)
 
 text {* Intervals of nats with @{text Suc} *}
 
-lemma atLeastLessThanSuc_atLeastAtMost: "{l..Suc u(} = {l..u}"
+lemma atLeastLessThanSuc_atLeastAtMost: "{l..<Suc u} = {l..u}"
   by (simp add: lessThan_Suc_atMost atLeastAtMost_def atLeastLessThan_def)
 
-lemma atLeastSucAtMost_greaterThanAtMost: "{Suc l..u} = {)l..u}"  
+lemma atLeastSucAtMost_greaterThanAtMost: "{Suc l..u} = {l<..u}"  
   by (simp add: atLeast_Suc_greaterThan atLeastAtMost_def 
     greaterThanAtMost_def)
 
-lemma atLeastSucLessThan_greaterThanLessThan: "{Suc l..u(} = {)l..u(}"  
+lemma atLeastSucLessThan_greaterThanLessThan: "{Suc l..<u} = {l<..<u}"  
   by (simp add: atLeast_Suc_greaterThan atLeastLessThan_def 
     greaterThanLessThan_def)
 
 subsubsection {* Finiteness *}
 
-lemma finite_lessThan [iff]: fixes k :: nat shows "finite {..k(}"
+lemma finite_lessThan [iff]: fixes k :: nat shows "finite {..<k}"
   by (induct k) (simp_all add: lessThan_Suc)
 
 lemma finite_atMost [iff]: fixes k :: nat shows "finite {..k}"
   by (induct k) (simp_all add: atMost_Suc)
 
 lemma finite_greaterThanLessThan [iff]:
-  fixes l :: nat shows "finite {)l..u(}"
+  fixes l :: nat shows "finite {l<..<u}"
 by (simp add: greaterThanLessThan_def)
 
 lemma finite_atLeastLessThan [iff]:
-  fixes l :: nat shows "finite {l..u(}"
+  fixes l :: nat shows "finite {l..<u}"
 by (simp add: atLeastLessThan_def)
 
 lemma finite_greaterThanAtMost [iff]:
-  fixes l :: nat shows "finite {)l..u}"
+  fixes l :: nat shows "finite {l<..u}"
 by (simp add: greaterThanAtMost_def)
 
 lemma finite_atLeastAtMost [iff]:
@@ -278,16 +292,16 @@
 
 subsubsection {* Cardinality *}
 
-lemma card_lessThan [simp]: "card {..u(} = u"
+lemma card_lessThan [simp]: "card {..<u} = u"
   by (induct_tac u, simp_all add: lessThan_Suc)
 
 lemma card_atMost [simp]: "card {..u} = Suc u"
   by (simp add: lessThan_Suc_atMost [THEN sym])
 
-lemma card_atLeastLessThan [simp]: "card {l..u(} = u - l"
-  apply (subgoal_tac "card {l..u(} = card {..u-l(}")
+lemma card_atLeastLessThan [simp]: "card {l..<u} = u - l"
+  apply (subgoal_tac "card {l..<u} = card {..<u-l}")
   apply (erule ssubst, rule card_lessThan)
-  apply (subgoal_tac "(%x. x + l) ` {..u-l(} = {l..u(}")
+  apply (subgoal_tac "(%x. x + l) ` {..<u-l} = {l..<u}")
   apply (erule subst)
   apply (rule card_image)
   apply (rule finite_lessThan)
@@ -301,52 +315,52 @@
 lemma card_atLeastAtMost [simp]: "card {l..u} = Suc u - l"
   by (subst atLeastLessThanSuc_atLeastAtMost [THEN sym], simp)
 
-lemma card_greaterThanAtMost [simp]: "card {)l..u} = u - l" 
+lemma card_greaterThanAtMost [simp]: "card {l<..u} = u - l" 
   by (subst atLeastSucAtMost_greaterThanAtMost [THEN sym], simp)
 
-lemma card_greaterThanLessThan [simp]: "card {)l..u(} = u - Suc l"
+lemma card_greaterThanLessThan [simp]: "card {l<..<u} = u - Suc l"
   by (subst atLeastSucLessThan_greaterThanLessThan [THEN sym], simp)
 
 subsection {* Intervals of integers *}
 
-lemma atLeastLessThanPlusOne_atLeastAtMost_int: "{l..u+1(} = {l..(u::int)}"
+lemma atLeastLessThanPlusOne_atLeastAtMost_int: "{l..<u+1} = {l..(u::int)}"
   by (auto simp add: atLeastAtMost_def atLeastLessThan_def)
 
-lemma atLeastPlusOneAtMost_greaterThanAtMost_int: "{l+1..u} = {)l..(u::int)}"  
+lemma atLeastPlusOneAtMost_greaterThanAtMost_int: "{l+1..u} = {l<..(u::int)}"  
   by (auto simp add: atLeastAtMost_def greaterThanAtMost_def)
 
 lemma atLeastPlusOneLessThan_greaterThanLessThan_int: 
-    "{l+1..u(} = {)l..(u::int)(}"  
+    "{l+1..<u} = {l<..<u::int}"  
   by (auto simp add: atLeastLessThan_def greaterThanLessThan_def)
 
 subsubsection {* Finiteness *}
 
 lemma image_atLeastZeroLessThan_int: "0 \<le> u ==> 
-    {(0::int)..u(} = int ` {..nat u(}"
+    {(0::int)..<u} = int ` {..<nat u}"
   apply (unfold image_def lessThan_def)
   apply auto
   apply (rule_tac x = "nat x" in exI)
   apply (auto simp add: zless_nat_conj zless_nat_eq_int_zless [THEN sym])
   done
 
-lemma finite_atLeastZeroLessThan_int: "finite {(0::int)..u(}"
+lemma finite_atLeastZeroLessThan_int: "finite {(0::int)..<u}"
   apply (case_tac "0 \<le> u")
   apply (subst image_atLeastZeroLessThan_int, assumption)
   apply (rule finite_imageI)
   apply auto
-  apply (subgoal_tac "{0..u(} = {}")
+  apply (subgoal_tac "{0..<u} = {}")
   apply auto
   done
 
 lemma image_atLeastLessThan_int_shift: 
-    "(%x. x + (l::int)) ` {0..u-l(} = {l..u(}"
+    "(%x. x + (l::int)) ` {0..<u-l} = {l..<u}"
   apply (auto simp add: image_def atLeastLessThan_iff)
   apply (rule_tac x = "x - l" in bexI)
   apply auto
   done
 
-lemma finite_atLeastLessThan_int [iff]: "finite {l..(u::int)(}"
-  apply (subgoal_tac "(%x. x + l) ` {0..u-l(} = {l..u(}")
+lemma finite_atLeastLessThan_int [iff]: "finite {l..<u::int}"
+  apply (subgoal_tac "(%x. x + l) ` {0..<u-l} = {l..<u}")
   apply (erule subst)
   apply (rule finite_imageI)
   apply (rule finite_atLeastZeroLessThan_int)
@@ -356,25 +370,25 @@
 lemma finite_atLeastAtMost_int [iff]: "finite {l..(u::int)}" 
   by (subst atLeastLessThanPlusOne_atLeastAtMost_int [THEN sym], simp)
 
-lemma finite_greaterThanAtMost_int [iff]: "finite {)l..(u::int)}" 
+lemma finite_greaterThanAtMost_int [iff]: "finite {l<..(u::int)}" 
   by (subst atLeastPlusOneAtMost_greaterThanAtMost_int [THEN sym], simp)
 
-lemma finite_greaterThanLessThan_int [iff]: "finite {)l..(u::int)(}" 
+lemma finite_greaterThanLessThan_int [iff]: "finite {l<..<u::int}" 
   by (subst atLeastPlusOneLessThan_greaterThanLessThan_int [THEN sym], simp)
 
 subsubsection {* Cardinality *}
 
-lemma card_atLeastZeroLessThan_int: "card {(0::int)..u(} = nat u"
+lemma card_atLeastZeroLessThan_int: "card {(0::int)..<u} = nat u"
   apply (case_tac "0 \<le> u")
   apply (subst image_atLeastZeroLessThan_int, assumption)
   apply (subst card_image)
   apply (auto simp add: inj_on_def)
   done
 
-lemma card_atLeastLessThan_int [simp]: "card {l..u(} = nat (u - l)"
-  apply (subgoal_tac "card {l..u(} = card {0..u-l(}")
+lemma card_atLeastLessThan_int [simp]: "card {l..<u} = nat (u - l)"
+  apply (subgoal_tac "card {l..<u} = card {0..<u-l}")
   apply (erule ssubst, rule card_atLeastZeroLessThan_int)
-  apply (subgoal_tac "(%x. x + l) ` {0..u-l(} = {l..u(}")
+  apply (subgoal_tac "(%x. x + l) ` {0..<u-l} = {l..<u}")
   apply (erule subst)
   apply (rule card_image)
   apply (rule finite_atLeastZeroLessThan_int)
@@ -387,10 +401,10 @@
   apply (auto simp add: compare_rls)
   done
 
-lemma card_greaterThanAtMost_int [simp]: "card {)l..u} = nat (u - l)" 
+lemma card_greaterThanAtMost_int [simp]: "card {l<..u} = nat (u - l)" 
   by (subst atLeastPlusOneAtMost_greaterThanAtMost_int [THEN sym], simp)
 
-lemma card_greaterThanLessThan_int [simp]: "card {)l..u(} = nat (u - (l + 1))"
+lemma card_greaterThanLessThan_int [simp]: "card {l<..<u} = nat (u - (l + 1))"
   by (subst atLeastPlusOneLessThan_greaterThanLessThan_int [THEN sym], simp)
 
 
@@ -403,38 +417,38 @@
 text {* Singletons and open intervals *}
 
 lemma ivl_disj_un_singleton:
-  "{l::'a::linorder} Un {)l..} = {l..}"
-  "{..u(} Un {u::'a::linorder} = {..u}"
-  "(l::'a::linorder) < u ==> {l} Un {)l..u(} = {l..u(}"
-  "(l::'a::linorder) < u ==> {)l..u(} Un {u} = {)l..u}"
-  "(l::'a::linorder) <= u ==> {l} Un {)l..u} = {l..u}"
-  "(l::'a::linorder) <= u ==> {l..u(} Un {u} = {l..u}"
+  "{l::'a::linorder} Un {l<..} = {l..}"
+  "{..<u} Un {u::'a::linorder} = {..u}"
+  "(l::'a::linorder) < u ==> {l} Un {l<..<u} = {l..<u}"
+  "(l::'a::linorder) < u ==> {l<..<u} Un {u} = {l<..u}"
+  "(l::'a::linorder) <= u ==> {l} Un {l<..u} = {l..u}"
+  "(l::'a::linorder) <= u ==> {l..<u} Un {u} = {l..u}"
 by auto
 
 text {* One- and two-sided intervals *}
 
 lemma ivl_disj_un_one:
-  "(l::'a::linorder) < u ==> {..l} Un {)l..u(} = {..u(}"
-  "(l::'a::linorder) <= u ==> {..l(} Un {l..u(} = {..u(}"
-  "(l::'a::linorder) <= u ==> {..l} Un {)l..u} = {..u}"
-  "(l::'a::linorder) <= u ==> {..l(} Un {l..u} = {..u}"
-  "(l::'a::linorder) <= u ==> {)l..u} Un {)u..} = {)l..}"
-  "(l::'a::linorder) < u ==> {)l..u(} Un {u..} = {)l..}"
-  "(l::'a::linorder) <= u ==> {l..u} Un {)u..} = {l..}"
-  "(l::'a::linorder) <= u ==> {l..u(} Un {u..} = {l..}"
+  "(l::'a::linorder) < u ==> {..l} Un {l<..<u} = {..<u}"
+  "(l::'a::linorder) <= u ==> {..<l} Un {l..<u} = {..<u}"
+  "(l::'a::linorder) <= u ==> {..l} Un {l<..u} = {..u}"
+  "(l::'a::linorder) <= u ==> {..<l} Un {l..u} = {..u}"
+  "(l::'a::linorder) <= u ==> {l<..u} Un {u<..} = {l<..}"
+  "(l::'a::linorder) < u ==> {l<..<u} Un {u..} = {l<..}"
+  "(l::'a::linorder) <= u ==> {l..u} Un {u<..} = {l..}"
+  "(l::'a::linorder) <= u ==> {l..<u} Un {u..} = {l..}"
 by auto
 
 text {* Two- and two-sided intervals *}
 
 lemma ivl_disj_un_two:
-  "[| (l::'a::linorder) < m; m <= u |] ==> {)l..m(} Un {m..u(} = {)l..u(}"
-  "[| (l::'a::linorder) <= m; m < u |] ==> {)l..m} Un {)m..u(} = {)l..u(}"
-  "[| (l::'a::linorder) <= m; m <= u |] ==> {l..m(} Un {m..u(} = {l..u(}"
-  "[| (l::'a::linorder) <= m; m < u |] ==> {l..m} Un {)m..u(} = {l..u(}"
-  "[| (l::'a::linorder) < m; m <= u |] ==> {)l..m(} Un {m..u} = {)l..u}"
-  "[| (l::'a::linorder) <= m; m <= u |] ==> {)l..m} Un {)m..u} = {)l..u}"
-  "[| (l::'a::linorder) <= m; m <= u |] ==> {l..m(} Un {m..u} = {l..u}"
-  "[| (l::'a::linorder) <= m; m <= u |] ==> {l..m} Un {)m..u} = {l..u}"
+  "[| (l::'a::linorder) < m; m <= u |] ==> {l<..<m} Un {m..<u} = {l<..<u}"
+  "[| (l::'a::linorder) <= m; m < u |] ==> {l<..m} Un {m<..<u} = {l<..<u}"
+  "[| (l::'a::linorder) <= m; m <= u |] ==> {l..<m} Un {m..<u} = {l..<u}"
+  "[| (l::'a::linorder) <= m; m < u |] ==> {l..m} Un {m<..<u} = {l..<u}"
+  "[| (l::'a::linorder) < m; m <= u |] ==> {l<..<m} Un {m..u} = {l<..u}"
+  "[| (l::'a::linorder) <= m; m <= u |] ==> {l<..m} Un {m<..u} = {l<..u}"
+  "[| (l::'a::linorder) <= m; m <= u |] ==> {l..<m} Un {m..u} = {l..u}"
+  "[| (l::'a::linorder) <= m; m <= u |] ==> {l..m} Un {m<..u} = {l..u}"
 by auto
 
 lemmas ivl_disj_un = ivl_disj_un_singleton ivl_disj_un_one ivl_disj_un_two
@@ -444,38 +458,38 @@
 text {* Singletons and open intervals *}
 
 lemma ivl_disj_int_singleton:
-  "{l::'a::order} Int {)l..} = {}"
-  "{..u(} Int {u} = {}"
-  "{l} Int {)l..u(} = {}"
-  "{)l..u(} Int {u} = {}"
-  "{l} Int {)l..u} = {}"
-  "{l..u(} Int {u} = {}"
+  "{l::'a::order} Int {l<..} = {}"
+  "{..<u} Int {u} = {}"
+  "{l} Int {l<..<u} = {}"
+  "{l<..<u} Int {u} = {}"
+  "{l} Int {l<..u} = {}"
+  "{l..<u} Int {u} = {}"
   by simp+
 
 text {* One- and two-sided intervals *}
 
 lemma ivl_disj_int_one:
-  "{..l::'a::order} Int {)l..u(} = {}"
-  "{..l(} Int {l..u(} = {}"
-  "{..l} Int {)l..u} = {}"
-  "{..l(} Int {l..u} = {}"
-  "{)l..u} Int {)u..} = {}"
-  "{)l..u(} Int {u..} = {}"
-  "{l..u} Int {)u..} = {}"
-  "{l..u(} Int {u..} = {}"
+  "{..l::'a::order} Int {l<..<u} = {}"
+  "{..<l} Int {l..<u} = {}"
+  "{..l} Int {l<..u} = {}"
+  "{..<l} Int {l..u} = {}"
+  "{l<..u} Int {u<..} = {}"
+  "{l<..<u} Int {u..} = {}"
+  "{l..u} Int {u<..} = {}"
+  "{l..<u} Int {u..} = {}"
   by auto
 
 text {* Two- and two-sided intervals *}
 
 lemma ivl_disj_int_two:
-  "{)l::'a::order..m(} Int {m..u(} = {}"
-  "{)l..m} Int {)m..u(} = {}"
-  "{l..m(} Int {m..u(} = {}"
-  "{l..m} Int {)m..u(} = {}"
-  "{)l..m(} Int {m..u} = {}"
-  "{)l..m} Int {)m..u} = {}"
-  "{l..m(} Int {m..u} = {}"
-  "{l..m} Int {)m..u} = {}"
+  "{l::'a::order<..<m} Int {m..<u} = {}"
+  "{l<..m} Int {m<..<u} = {}"
+  "{l..<m} Int {m..<u} = {}"
+  "{l..m} Int {m<..<u} = {}"
+  "{l<..<m} Int {m..u} = {}"
+  "{l<..m} Int {m<..u} = {}"
+  "{l..<m} Int {m..u} = {}"
+  "{l..m} Int {m<..u} = {}"
   by auto
 
 lemmas ivl_disj_int = ivl_disj_int_singleton ivl_disj_int_one ivl_disj_int_two
@@ -504,7 +518,7 @@
 syntax
   "_Summation" :: "idt => 'a => 'b => 'b"    ("\<Sum>_<_. _" [0, 51, 10] 10)
 translations
-  "\<Sum>i < n. b" == "setsum (\<lambda>i. b) {..n(}"
+  "\<Sum>i < n. b" == "setsum (\<lambda>i. b) {..<n}"
 
 lemma Summation_Suc[simp]: "(\<Sum>i < Suc n. b i) = b n + (\<Sum>i < n. b i)"
 by (simp add:lessThan_Suc)
diff -r f224d27bb1f8 -r d59f7e2e18d3 src/HOL/UNITY/Comp/AllocBase.thy
--- a/src/HOL/UNITY/Comp/AllocBase.thy	Thu Jul 15 08:38:37 2004 +0200
+++ b/src/HOL/UNITY/Comp/AllocBase.thy	Thu Jul 15 13:11:34 2004 +0200
@@ -87,8 +87,8 @@
 lemma bag_of_sublist_Un_Int:
      "bag_of (sublist l (A Un B)) + bag_of (sublist l (A Int B)) =  
       bag_of (sublist l A) + bag_of (sublist l B)"
-apply (subgoal_tac "A Int B Int {..length l (} =
-	            (A Int {..length l (}) Int (B Int {..length l (}) ")
+apply (subgoal_tac "A Int B Int {..<length l} =
+	            (A Int {..<length l}) Int (B Int {..<length l}) ")
 apply (simp add: bag_of_sublist Int_Un_distrib2 setsum_Un_Int, blast)
 done
 
diff -r f224d27bb1f8 -r d59f7e2e18d3 src/HOL/UNITY/WFair.thy
--- a/src/HOL/UNITY/WFair.thy	Thu Jul 15 08:38:37 2004 +0200
+++ b/src/HOL/UNITY/WFair.thy	Thu Jul 15 13:11:34 2004 +0200
@@ -470,7 +470,7 @@
 
 (*Alternative proof is via the lemma F \<in> (A \<inter> f-`(lessThan m)) leadsTo B*)
 lemma lessThan_induct: 
-     "[| !!m::nat. F \<in> (A \<inter> f-`{m}) leadsTo ((A \<inter> f-`{..m(}) \<union> B) |]  
+     "[| !!m::nat. F \<in> (A \<inter> f-`{m}) leadsTo ((A \<inter> f-`{..<m}) \<union> B) |]  
       ==> F \<in> A leadsTo B"
 apply (rule wf_less_than [THEN leadsTo_wf_induct])
 apply (simp (no_asm_simp))
diff -r f224d27bb1f8 -r d59f7e2e18d3 src/HOL/ex/NatSum.thy
--- a/src/HOL/ex/NatSum.thy	Thu Jul 15 08:38:37 2004 +0200
+++ b/src/HOL/ex/NatSum.thy	Thu Jul 15 13:11:34 2004 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/ex/NatSum.ML
+(* Title: HOL/ex/NatSum.ML
     ID:         $Id$
     Author:     Tobias Nipkow
 *)
@@ -26,7 +26,7 @@
   squared.
 *}
 
-lemma sum_of_odds: "(\<Sum>i \<in> {..n(}. Suc (i + i)) = n * n"
+lemma sum_of_odds: "(\<Sum>i \<in> {..<n}. Suc (i + i)) = n * n"
   apply (induct n)
    apply auto
   done
@@ -37,7 +37,7 @@
 *}
 
 lemma sum_of_odd_squares:
-  "3 * (\<Sum>i \<in> {..n(}. Suc (2*i) * Suc (2*i)) =
+  "3 * (\<Sum>i \<in> {..<n}. Suc (2*i) * Suc (2*i)) =
     n * (4 * n * n - 1)"
   apply (induct n)
    apply (auto split: nat_diff_split) (*eliminate the subtraction*)
@@ -51,7 +51,7 @@
 lemma numeral_2_eq_2: "2 = Suc (Suc 0)" by (auto ); 
 
 lemma sum_of_odd_cubes:
-  "(\<Sum>i \<in> {..n(}. Suc (2*i) * Suc (2*i) * Suc (2*i)) =
+  "(\<Sum>i \<in> {..<n}. Suc (2*i) * Suc (2*i) * Suc (2*i)) =
     n * n * (2 * n * n - 1)"
   apply (induct n)
    apply (auto split: nat_diff_split) (*eliminate the subtraction*)
@@ -105,7 +105,7 @@
   zdiff_zmult_distrib2 [simp]
 
 lemma int_sum_of_fourth_powers:
-  "30 * int (\<Sum>i \<in> {..m(}. i * i * i * i) =
+  "30 * int (\<Sum>i \<in> {..<m}. i * i * i * i) =
     int m * (int m - 1) * (int (2 * m) - 1) *
     (int (3 * m * m) - int (3 * m) - 1)"
   apply (induct m)
@@ -118,17 +118,17 @@
   general case.
 *}
 
-lemma sum_of_2_powers: "(\<Sum>i \<in> {..n(}. 2^i) = 2^n - (1::nat)"
+lemma sum_of_2_powers: "(\<Sum>i \<in> {..<n}. 2^i) = 2^n - (1::nat)"
   apply (induct n)
    apply (auto split: nat_diff_split)
   done
 
-lemma sum_of_3_powers: "2 * (\<Sum>i \<in> {..n(}. 3^i) = 3^n - (1::nat)"
+lemma sum_of_3_powers: "2 * (\<Sum>i \<in> {..<n}. 3^i) = 3^n - (1::nat)"
   apply (induct n)
    apply auto
   done
 
-lemma sum_of_powers: "0 < k ==> (k - 1) * (\<Sum>i \<in> {..n(}. k^i) = k^n - (1::nat)"
+lemma sum_of_powers: "0 < k ==> (k - 1) * (\<Sum>i \<in> {..<n}. k^i) = k^n - (1::nat)"
   apply (induct n)
    apply auto
   done