# HG changeset patch
# User wenzelm
# Date 1437600360 -7200
# Node ID ad5b4771fc19921598b34d75189418beb26e079f
# Parent  76560ce8dead6f741fce0efdb1f2b4118ac8e285
tuned proofs;

diff -r 76560ce8dead -r ad5b4771fc19 src/HOL/Decision_Procs/Commutative_Ring_Complete.thy
--- a/src/HOL/Decision_Procs/Commutative_Ring_Complete.thy	Wed Jul 22 14:55:42 2015 +0200
+++ b/src/HOL/Decision_Procs/Commutative_Ring_Complete.thy	Wed Jul 22 23:26:00 2015 +0200
@@ -212,7 +212,7 @@
     by atomize_elim arith
   then show ?case
   proof cases
-    case x: 1
+    case 1
     with 7 show ?thesis
       by (auto simp add: norm_Pinj_0_False)
   next
diff -r 76560ce8dead -r ad5b4771fc19 src/HOL/Decision_Procs/Ferrack.thy
--- a/src/HOL/Decision_Procs/Ferrack.thy	Wed Jul 22 14:55:42 2015 +0200
+++ b/src/HOL/Decision_Procs/Ferrack.thy	Wed Jul 22 23:26:00 2015 +0200
@@ -1726,7 +1726,7 @@
     by atomize_elim auto
   then show ?case
   proof cases
-    case y: 1
+    case 1
     then have "y * real c < - ?N x e"
       by (simp add: pos_less_divide_eq[OF cp, where a="y" and b="-?N x e", symmetric])
     then have "real c * y + ?N x e < 0"
@@ -1734,7 +1734,7 @@
     then show ?thesis
       using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"] by simp
   next
-    case y: 2
+    case 2
     with yu have eu: "u > (- ?N x e) / real c"
       by auto
     with noSc ly yu have "(- ?N x e) / real c \<le> l"
@@ -1759,7 +1759,7 @@
     by atomize_elim auto
   then show ?case
   proof cases
-    case y: 1
+    case 1
     then have "y * real c < - ?N x e"
       by (simp add: pos_less_divide_eq[OF cp, where a="y" and b="-?N x e", symmetric])
     then have "real c * y + ?N x e < 0"
@@ -1767,7 +1767,7 @@
     then show ?thesis
       using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"] by simp
   next
-    case y: 2
+    case 2
     with yu have eu: "u > (- ?N x e) / real c"
       by auto
     with noSc ly yu have "(- ?N x e) / real c \<le> l"