src/HOL/ex/Groebner_Examples.thy
changeset 25255 66ee31849d13
parent 23581 297c6d706322
child 26317 01a98fd72eae
     1.1 --- a/src/HOL/ex/Groebner_Examples.thy	Wed Oct 31 12:19:44 2007 +0100
     1.2 +++ b/src/HOL/ex/Groebner_Examples.thy	Wed Oct 31 12:19:45 2007 +0100
     1.3 @@ -6,7 +6,7 @@
     1.4  header {* Groebner Basis Examples *}
     1.5  
     1.6  theory Groebner_Examples
     1.7 -imports Main
     1.8 +imports Groebner_Basis
     1.9  begin
    1.10  
    1.11  subsection {* Basic examples *}
    1.12 @@ -98,4 +98,8 @@
    1.13    using assms 
    1.14    by (algebra add: collinear_def split_def fst_conv snd_conv)
    1.15  
    1.16 +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.17 +  apply algebra
    1.18 +  done
    1.19 +
    1.20  end