src/HOL/Groebner_Basis.thy
changeset 48891 c0eafbd55de3
parent 47432 e1576d13e933
child 54251 adea9f6986b2
     1.1 --- a/src/HOL/Groebner_Basis.thy	Wed Aug 22 22:47:16 2012 +0200
     1.2 +++ b/src/HOL/Groebner_Basis.thy	Wed Aug 22 22:55:41 2012 +0200
     1.3 @@ -6,8 +6,6 @@
     1.4  
     1.5  theory Groebner_Basis
     1.6  imports Semiring_Normalization
     1.7 -uses
     1.8 -  ("Tools/groebner.ML")
     1.9  begin
    1.10  
    1.11  subsection {* Groebner Bases *}
    1.12 @@ -41,7 +39,7 @@
    1.13  
    1.14  setup Algebra_Simplification.setup
    1.15  
    1.16 -use "Tools/groebner.ML"
    1.17 +ML_file "Tools/groebner.ML"
    1.18  
    1.19  method_setup algebra = {*
    1.20    let