src/HOL/ex/Groebner_Examples.thy
changeset 26317 01a98fd72eae
parent 25255 66ee31849d13
child 31021 53642251a04f
     1.1 --- a/src/HOL/ex/Groebner_Examples.thy	Tue Mar 18 20:33:31 2008 +0100
     1.2 +++ b/src/HOL/ex/Groebner_Examples.thy	Tue Mar 18 20:33:33 2008 +0100
     1.3 @@ -99,7 +99,6 @@
     1.4    by (algebra add: collinear_def split_def fst_conv snd_conv)
     1.5  
     1.6  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"
     1.7 -  apply algebra
     1.8 -  done
     1.9 +  by algebra
    1.10  
    1.11  end