src/HOL/Integ/reflected_presburger.ML
changeset 17426 acfc05e02e5b
parent 17401 9147c880ada6
     1.1 --- a/src/HOL/Integ/reflected_presburger.ML	Thu Sep 15 20:27:48 2005 +0200
     1.2 +++ b/src/HOL/Integ/reflected_presburger.ML	Thu Sep 15 20:38:47 2005 +0200
     1.3 @@ -52,7 +52,7 @@
     1.4      (if (c = 0) then Cst 0
     1.5        else Add (Mult (Cst (c * c'), Var n), lin_mul (c, r)));
     1.6  
     1.7 -fun op_60_def0 m n = ((m) < (n));
     1.8 +fun op_60_def0 m n = IntInf.< (m,n);
     1.9  
    1.10  fun op_60_61_def0 m n = not (op_60_def0 n m);
    1.11  
    1.12 @@ -174,7 +174,7 @@
    1.13    | nnf (NOT (Equ (p, q))) =
    1.14      Or (And (nnf p, nnf (NOT q)), And (nnf (NOT p), nnf q));
    1.15  
    1.16 -fun op_45_def2 z w = (z + ~ w);
    1.17 +fun op_45_def2 z w =  IntInf.+ (z,~ w);
    1.18  
    1.19  fun op_45_def0 m n = nat (op_45_def2 (m) (n));
    1.20  
    1.21 @@ -215,7 +215,7 @@
    1.22  
    1.23  fun split x = (fn p => x (fst p) (snd p));
    1.24  
    1.25 -fun negateSnd x = split (fn q => fn r => (q, ~ r)) x;
    1.26 +fun negateSnd x = split (fn q => fn r => (q, IntInf.~ r)) x;
    1.27  
    1.28  fun adjust b =
    1.29    (fn (q:IntInf.int, r:IntInf.int) =>
    1.30 @@ -240,7 +240,7 @@
    1.31                     else negateSnd (posDivAlg (~ a, ~ b)))))
    1.32      x;
    1.33  
    1.34 -fun op_mod_def1 (a:IntInf.int) (b:IntInf.int) = snd (divAlg (a, b));
    1.35 +fun op_mod_def1 a b = snd (divAlg (a, b));
    1.36  
    1.37  fun op_dvd m n = (op_mod_def1 n m = 0);
    1.38  
    1.39 @@ -1139,9 +1139,9 @@
    1.40    | minusinf (QAll ap) = QAll ap
    1.41    | minusinf (QEx aq) = QEx aq;
    1.42  
    1.43 -fun (abs: IntInf.int -> IntInf.int) i = (if (i < 0) then ~ i else i);
    1.44 +fun abs (i:IntInf.int) = (if (i < 0) then IntInf.~ i else i);
    1.45  
    1.46 -fun op_div_def1 (a:IntInf.int) (b:IntInf.int) = fst (divAlg (a, b));
    1.47 +fun op_div_def1 a b = fst (divAlg (a, b));
    1.48  
    1.49  fun op_mod_def0 m n = nat (op_mod_def1 (m) (n));
    1.50