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