tuned proofs;
authorwenzelm
Wed Jul 22 23:26:00 2015 +0200 (2015-07-22)
changeset 60767ad5b4771fc19
parent 60766 76560ce8dead
child 60768 f47bd91fdc75
tuned proofs;
src/HOL/Decision_Procs/Commutative_Ring_Complete.thy
src/HOL/Decision_Procs/Ferrack.thy
     1.1 --- a/src/HOL/Decision_Procs/Commutative_Ring_Complete.thy	Wed Jul 22 14:55:42 2015 +0200
     1.2 +++ b/src/HOL/Decision_Procs/Commutative_Ring_Complete.thy	Wed Jul 22 23:26:00 2015 +0200
     1.3 @@ -212,7 +212,7 @@
     1.4      by atomize_elim arith
     1.5    then show ?case
     1.6    proof cases
     1.7 -    case x: 1
     1.8 +    case 1
     1.9      with 7 show ?thesis
    1.10        by (auto simp add: norm_Pinj_0_False)
    1.11    next
     2.1 --- a/src/HOL/Decision_Procs/Ferrack.thy	Wed Jul 22 14:55:42 2015 +0200
     2.2 +++ b/src/HOL/Decision_Procs/Ferrack.thy	Wed Jul 22 23:26:00 2015 +0200
     2.3 @@ -1726,7 +1726,7 @@
     2.4      by atomize_elim auto
     2.5    then show ?case
     2.6    proof cases
     2.7 -    case y: 1
     2.8 +    case 1
     2.9      then have "y * real c < - ?N x e"
    2.10        by (simp add: pos_less_divide_eq[OF cp, where a="y" and b="-?N x e", symmetric])
    2.11      then have "real c * y + ?N x e < 0"
    2.12 @@ -1734,7 +1734,7 @@
    2.13      then show ?thesis
    2.14        using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"] by simp
    2.15    next
    2.16 -    case y: 2
    2.17 +    case 2
    2.18      with yu have eu: "u > (- ?N x e) / real c"
    2.19        by auto
    2.20      with noSc ly yu have "(- ?N x e) / real c \<le> l"
    2.21 @@ -1759,7 +1759,7 @@
    2.22      by atomize_elim auto
    2.23    then show ?case
    2.24    proof cases
    2.25 -    case y: 1
    2.26 +    case 1
    2.27      then have "y * real c < - ?N x e"
    2.28        by (simp add: pos_less_divide_eq[OF cp, where a="y" and b="-?N x e", symmetric])
    2.29      then have "real c * y + ?N x e < 0"
    2.30 @@ -1767,7 +1767,7 @@
    2.31      then show ?thesis
    2.32        using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"] by simp
    2.33    next
    2.34 -    case y: 2
    2.35 +    case 2
    2.36      with yu have eu: "u > (- ?N x e) / real c"
    2.37        by auto
    2.38      with noSc ly yu have "(- ?N x e) / real c \<le> l"