changeset 60767 | ad5b4771fc19 |
parent 60708 | f425e80a3eb0 |
child 61586 | 5197a2ecb658 |
--- 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