# HG changeset patch
# User chaieb
# Date 1131702599 -3600
# Node ID e5ab63ca6b0f2f56bb97cfb580b14d0f25d838dc
# Parent  0c05abaf6244814ccbb0d22f575fd5badfab0511
old argument "abs" is replaced by "no_abs". Abstraction is turned on by default.

diff -r 0c05abaf6244 -r e5ab63ca6b0f src/HOL/Integ/presburger.ML
--- a/src/HOL/Integ/presburger.ML	Fri Nov 11 00:09:37 2005 +0100
+++ b/src/HOL/Integ/presburger.ML	Fri Nov 11 10:49:59 2005 +0100
@@ -295,11 +295,11 @@
 fun presburger_args meth =
  let val parse_flag = 
          Args.$$$ "no_quantify" >> K (apfst (K false))
-      || Args.$$$ "abs" >> K (apsnd (K true));
+      || Args.$$$ "no_abs" >> K (apsnd (K false));
  in
    Method.simple_args 
   (Scan.optional (Args.$$$ "(" |-- Scan.repeat1 parse_flag --| Args.$$$ ")") [] >>
-    curry (Library.foldl op |>) (true, false))
+    curry (Library.foldl op |>) (true, true))
     (fn (q,a) => fn _ => meth q a 1)
   end;
 
@@ -312,8 +312,8 @@
      "decision procedure for Presburger arithmetic"),
    ArithTheoryData.map (fn {splits, inj_consts, discrete, presburger} =>
      {splits = splits, inj_consts = inj_consts, discrete = discrete,
-      presburger = SOME (presburger_tac true false)})];
+      presburger = SOME (presburger_tac true true)})];
 
 end;
 
-val presburger_tac = Presburger.presburger_tac true false;
+val presburger_tac = Presburger.presburger_tac true true;
diff -r 0c05abaf6244 -r e5ab63ca6b0f src/HOL/Tools/Presburger/presburger.ML
--- a/src/HOL/Tools/Presburger/presburger.ML	Fri Nov 11 00:09:37 2005 +0100
+++ b/src/HOL/Tools/Presburger/presburger.ML	Fri Nov 11 10:49:59 2005 +0100
@@ -295,11 +295,11 @@
 fun presburger_args meth =
  let val parse_flag = 
          Args.$$$ "no_quantify" >> K (apfst (K false))
-      || Args.$$$ "abs" >> K (apsnd (K true));
+      || Args.$$$ "no_abs" >> K (apsnd (K false));
  in
    Method.simple_args 
   (Scan.optional (Args.$$$ "(" |-- Scan.repeat1 parse_flag --| Args.$$$ ")") [] >>
-    curry (Library.foldl op |>) (true, false))
+    curry (Library.foldl op |>) (true, true))
     (fn (q,a) => fn _ => meth q a 1)
   end;
 
@@ -312,8 +312,8 @@
      "decision procedure for Presburger arithmetic"),
    ArithTheoryData.map (fn {splits, inj_consts, discrete, presburger} =>
      {splits = splits, inj_consts = inj_consts, discrete = discrete,
-      presburger = SOME (presburger_tac true false)})];
+      presburger = SOME (presburger_tac true true)})];
 
 end;
 
-val presburger_tac = Presburger.presburger_tac true false;
+val presburger_tac = Presburger.presburger_tac true true;