getting it work for SMLNJ
authorchaieb
Thu Sep 15 20:38:47 2005 +0200 (2005-09-15)
changeset 17426acfc05e02e5b
parent 17425 67c84a7d29f7
child 17427 3c45d890d47c
getting it work for SMLNJ
src/HOL/Integ/reflected_presburger.ML
src/HOL/Tools/Presburger/reflected_presburger.ML
     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  
     2.1 --- a/src/HOL/Tools/Presburger/reflected_presburger.ML	Thu Sep 15 20:27:48 2005 +0200
     2.2 +++ b/src/HOL/Tools/Presburger/reflected_presburger.ML	Thu Sep 15 20:38:47 2005 +0200
     2.3 @@ -52,7 +52,7 @@
     2.4      (if (c = 0) then Cst 0
     2.5        else Add (Mult (Cst (c * c'), Var n), lin_mul (c, r)));
     2.6  
     2.7 -fun op_60_def0 m n = ((m) < (n));
     2.8 +fun op_60_def0 m n = IntInf.< (m,n);
     2.9  
    2.10  fun op_60_61_def0 m n = not (op_60_def0 n m);
    2.11  
    2.12 @@ -174,7 +174,7 @@
    2.13    | nnf (NOT (Equ (p, q))) =
    2.14      Or (And (nnf p, nnf (NOT q)), And (nnf (NOT p), nnf q));
    2.15  
    2.16 -fun op_45_def2 z w = (z + ~ w);
    2.17 +fun op_45_def2 z w =  IntInf.+ (z,~ w);
    2.18  
    2.19  fun op_45_def0 m n = nat (op_45_def2 (m) (n));
    2.20  
    2.21 @@ -215,7 +215,7 @@
    2.22  
    2.23  fun split x = (fn p => x (fst p) (snd p));
    2.24  
    2.25 -fun negateSnd x = split (fn q => fn r => (q, ~ r)) x;
    2.26 +fun negateSnd x = split (fn q => fn r => (q, IntInf.~ r)) x;
    2.27  
    2.28  fun adjust b =
    2.29    (fn (q:IntInf.int, r:IntInf.int) =>
    2.30 @@ -240,7 +240,7 @@
    2.31                     else negateSnd (posDivAlg (~ a, ~ b)))))
    2.32      x;
    2.33  
    2.34 -fun op_mod_def1 (a:IntInf.int) (b:IntInf.int) = snd (divAlg (a, b));
    2.35 +fun op_mod_def1 a b = snd (divAlg (a, b));
    2.36  
    2.37  fun op_dvd m n = (op_mod_def1 n m = 0);
    2.38  
    2.39 @@ -1139,9 +1139,9 @@
    2.40    | minusinf (QAll ap) = QAll ap
    2.41    | minusinf (QEx aq) = QEx aq;
    2.42  
    2.43 -fun (abs: IntInf.int -> IntInf.int) i = (if (i < 0) then ~ i else i);
    2.44 +fun abs (i:IntInf.int) = (if (i < 0) then IntInf.~ i else i);
    2.45  
    2.46 -fun op_div_def1 (a:IntInf.int) (b:IntInf.int) = fst (divAlg (a, b));
    2.47 +fun op_div_def1 a b = fst (divAlg (a, b));
    2.48  
    2.49  fun op_mod_def0 m n = nat (op_mod_def1 (m) (n));
    2.50