changeset 26317 | 01a98fd72eae |
parent 25255 | 66ee31849d13 |
child 31021 | 53642251a04f |
--- a/src/HOL/ex/Groebner_Examples.thy Tue Mar 18 20:33:31 2008 +0100 +++ b/src/HOL/ex/Groebner_Examples.thy Tue Mar 18 20:33:33 2008 +0100 @@ -99,7 +99,6 @@ by (algebra add: collinear_def split_def fst_conv snd_conv) lemma "EX (d::int). a*y - a*x = n*d \<Longrightarrow> EX u v. a*u + n*v = 1 \<Longrightarrow> EX e. y - x = n*e" - apply algebra - done + by algebra end