changeset 56073 | 29e308b56d23 |
parent 56066 | cce36efe32eb |
child 56198 | 21dd034523e5 |
--- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy Wed Mar 12 22:57:50 2014 +0100 +++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy Thu Mar 13 07:07:07 2014 +0100 @@ -473,7 +473,6 @@ then have ?case using 4 apply (cases "p +\<^sub>p p' = 0\<^sub>p") apply (auto simp add: Let_def) - apply blast done } ultimately have ?case by blast