src/HOL/Presburger.thy
changeset 28290 4cc2b6046258
parent 27668 6eb20b2cecf8
child 28402 09e4aa3ddc25
     1.1 --- a/src/HOL/Presburger.thy	Thu Sep 18 14:06:58 2008 +0200
     1.2 +++ b/src/HOL/Presburger.thy	Thu Sep 18 19:39:44 2008 +0200
     1.3 @@ -440,7 +440,7 @@
     1.4  by simp_all
     1.5  
     1.6  use "Tools/Qelim/cooper.ML"
     1.7 -oracle linzqe_oracle ("term") = Coopereif.cooper_oracle
     1.8 +oracle linzqe_oracle = Coopereif.cooper_oracle
     1.9  
    1.10  use "Tools/Qelim/presburger.ML"
    1.11