# HG changeset patch
# User chaieb
# Date 1126727067 -7200
# Node ID ec9997d0a3ff1c2a6ab6f49529fa48dbfdca1ed9
# Parent  8d143599daa97b27092b3dc0963dc5a28b943d05
tactic and the rest eliminated, just the theory....

diff -r 8d143599daa9 -r ec9997d0a3ff src/HOL/ex/Reflected_Presburger.thy
--- a/src/HOL/ex/Reflected_Presburger.thy	Wed Sep 14 21:35:46 2005 +0200
+++ b/src/HOL/ex/Reflected_Presburger.thy	Wed Sep 14 21:44:27 2005 +0200
@@ -4,7 +4,7 @@
 
 theory Reflected_Presburger
 imports Main
-uses ("rcooper.ML") ("rpresbtac.ML")
+(* uses ("rcooper.ML") ("rpresbtac.ML") *)
 begin
 
 (* Shadow syntax for integer terms *)
@@ -5717,10 +5717,9 @@
 
 (*
 generate_code ("presburger.ML") test = "pa"
-*)
 use "rcooper.ML"
 oracle rpresburger_oracle ("term") = RCooper.rpresburger_oracle
 use "rpresbtac.ML"
 setup RPresburger.setup
-
+*)
 end