--- a/src/HOL/Integ/presburger.ML Mon Jun 14 14:20:55 2004 +0200
+++ b/src/HOL/Integ/presburger.ML Mon Jun 14 16:46:48 2004 +0200
@@ -28,6 +28,13 @@
(* Here still only one problem : The proof for the arithmetical transformations done on the dvd atomic formulae*)
(*-----------------------------------------------------------------*)
+
+(* Invoking the oracle *)
+
+fun pres_oracle sg t =
+ invoke_oracle (the_context()) "presburger_oracle"
+ (sg, CooperDec.COOPER_ORACLE t) ;
+
val presburger_ss = simpset_of (theory "Presburger");
fun cooper_pp sg (fm as e$Abs(xn,xT,p)) =
@@ -270,8 +277,11 @@
let val pth =
(* If quick_and_dirty then run without proof generation as oracle*)
if !quick_and_dirty
- then assume (cterm_of sg
+ then pres_oracle sg (Pattern.eta_long [] t1)
+(*
+assume (cterm_of sg
(HOLogic.mk_Trueprop(HOLogic.mk_eq(t1,CooperDec.integer_qelim (Pattern.eta_long [] t1)))))
+*)
else tmproof_of_int_qelim sg (Pattern.eta_long [] t1)
in
(trace_msg ("calling procedure with term:\n" ^