# HG changeset patch
# User chaieb
# Date 1085591169 -7200
# Node ID 9144ec118703269f104e26210536ce7ff71d3e78
# Parent  4b4b97d2937098ecd2c72cc416cae4afffd9ca2b
abstraction over functions is no default any more.

diff -r 4b4b97d29370 -r 9144ec118703 src/HOL/Integ/presburger.ML
--- a/src/HOL/Integ/presburger.ML	Wed May 26 18:52:18 2004 +0200
+++ b/src/HOL/Integ/presburger.ML	Wed May 26 19:06:09 2004 +0200
@@ -6,7 +6,7 @@
 Tactic for solving arithmetical Goals in Presburger Arithmetic
 *)
 
-(* This version of presburger deals with occurences of functional symbols in the subgoal and abstract over them to try to prove the more general formula. It then resolves with the subgoal. To disable this feature call the procedure with the parameter no_abs
+(* This version of presburger deals with occurences of functional symbols in the subgoal and abstract over them to try to prove the more general formula. It then resolves with the subgoal. To enable this feature call the procedure with the parameter abs
 *)
 
 signature PRESBURGER = 
@@ -279,11 +279,11 @@
 fun presburger_args meth =
  let val parse_flag = 
          Args.$$$ "no_quantify" >> K (apfst (K false))
-      || Args.$$$ "no_abs" >> K (apsnd (K false));
+      || Args.$$$ "abs" >> K (apsnd (K true));
  in
    Method.simple_args 
   (Scan.optional (Args.$$$ "(" |-- Args.list1 parse_flag --| Args.$$$ ")") [] >>
-    curry (foldl op |>) (true, true))
+    curry (foldl op |>) (true, false))
     (fn (q,a) => fn _ => meth q a 1)
   end;
 
@@ -296,7 +296,7 @@
      "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 true)})];
+      presburger = Some (presburger_tac true false)})];
 
 end;
 
diff -r 4b4b97d29370 -r 9144ec118703 src/HOL/Tools/Presburger/presburger.ML
--- a/src/HOL/Tools/Presburger/presburger.ML	Wed May 26 18:52:18 2004 +0200
+++ b/src/HOL/Tools/Presburger/presburger.ML	Wed May 26 19:06:09 2004 +0200
@@ -6,7 +6,7 @@
 Tactic for solving arithmetical Goals in Presburger Arithmetic
 *)
 
-(* This version of presburger deals with occurences of functional symbols in the subgoal and abstract over them to try to prove the more general formula. It then resolves with the subgoal. To disable this feature call the procedure with the parameter no_abs
+(* This version of presburger deals with occurences of functional symbols in the subgoal and abstract over them to try to prove the more general formula. It then resolves with the subgoal. To enable this feature call the procedure with the parameter abs
 *)
 
 signature PRESBURGER = 
@@ -279,11 +279,11 @@
 fun presburger_args meth =
  let val parse_flag = 
          Args.$$$ "no_quantify" >> K (apfst (K false))
-      || Args.$$$ "no_abs" >> K (apsnd (K false));
+      || Args.$$$ "abs" >> K (apsnd (K true));
  in
    Method.simple_args 
   (Scan.optional (Args.$$$ "(" |-- Args.list1 parse_flag --| Args.$$$ ")") [] >>
-    curry (foldl op |>) (true, true))
+    curry (foldl op |>) (true, false))
     (fn (q,a) => fn _ => meth q a 1)
   end;
 
@@ -296,7 +296,7 @@
      "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 true)})];
+      presburger = Some (presburger_tac true false)})];
 
 end;