# HG changeset patch
# User wenzelm
# Date 1634330947 -7200
# Node ID b4660c388e724b13e16ce0f4115fdb10c94d4262
# Parent  823ccd84b8795c785912b8797084fad6fbba3034
isabelle regenerate_cooper;

diff -r 823ccd84b879 -r b4660c388e72 src/HOL/Tools/Qelim/cooper.ML
--- a/src/HOL/Tools/Qelim/cooper.ML	Fri Oct 15 22:00:28 2021 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML	Fri Oct 15 22:49:07 2021 +0200
@@ -640,7 +640,7 @@
   | fm_of_term ps vs (\<^term>\<open>(=) :: bool => _ \<close> $ t1 $ t2) =
       Proc.Iff (fm_of_term ps vs t1, fm_of_term ps vs t2)
   | fm_of_term ps vs (Const (\<^const_name>\<open>Not\<close>, _) $ t') =
-      Proc.NOT (fm_of_term ps vs t')
+      Proc.Not (fm_of_term ps vs t')
   | fm_of_term ps vs (Const (\<^const_name>\<open>Ex\<close>, _) $ Abs abs) =
       Proc.E (uncurry (fm_of_term ps) (descend vs abs))
   | fm_of_term ps vs (Const (\<^const_name>\<open>All\<close>, _) $ Abs abs) =
@@ -677,18 +677,18 @@
   | term_of_fm ps vs (Proc.Or (t1, t2)) = HOLogic.disj $ term_of_fm ps vs t1 $ term_of_fm ps vs t2
   | term_of_fm ps vs (Proc.Imp (t1, t2)) = HOLogic.imp $ term_of_fm ps vs t1 $ term_of_fm ps vs t2
   | term_of_fm ps vs (Proc.Iff (t1, t2)) = \<^term>\<open>(=) :: bool => _\<close> $ term_of_fm ps vs t1 $ term_of_fm ps vs t2
-  | term_of_fm ps vs (Proc.NOT t') = HOLogic.Not $ term_of_fm ps vs t'
+  | term_of_fm ps vs (Proc.Not t') = HOLogic.Not $ term_of_fm ps vs t'
   | term_of_fm ps vs (Proc.Eq t') = \<^term>\<open>(=) :: int => _ \<close> $ term_of_num vs t'$ \<^term>\<open>0::int\<close>
-  | term_of_fm ps vs (Proc.NEq t') = term_of_fm ps vs (Proc.NOT (Proc.Eq t'))
+  | term_of_fm ps vs (Proc.NEq t') = term_of_fm ps vs (Proc.Not (Proc.Eq t'))
   | term_of_fm ps vs (Proc.Lt t') = \<^term>\<open>(<) :: int => _ \<close> $ term_of_num vs t' $ \<^term>\<open>0::int\<close>
   | term_of_fm ps vs (Proc.Le t') = \<^term>\<open>(<=) :: int => _ \<close> $ term_of_num vs t' $ \<^term>\<open>0::int\<close>
   | term_of_fm ps vs (Proc.Gt t') = \<^term>\<open>(<) :: int => _ \<close> $ \<^term>\<open>0::int\<close> $ term_of_num vs t'
   | term_of_fm ps vs (Proc.Ge t') = \<^term>\<open>(<=) :: int => _ \<close> $ \<^term>\<open>0::int\<close> $ term_of_num vs t'
   | term_of_fm ps vs (Proc.Dvd (i, t')) = \<^term>\<open>(dvd) :: int => _ \<close> $
       HOLogic.mk_number HOLogic.intT (Proc.integer_of_int i) $ term_of_num vs t'
-  | term_of_fm ps vs (Proc.NDvd (i, t')) = term_of_fm ps vs (Proc.NOT (Proc.Dvd (i, t')))
+  | term_of_fm ps vs (Proc.NDvd (i, t')) = term_of_fm ps vs (Proc.Not (Proc.Dvd (i, t')))
   | term_of_fm ps vs (Proc.Closed n) = nth ps (Proc.integer_of_nat n)
-  | term_of_fm ps vs (Proc.NClosed n) = term_of_fm ps vs (Proc.NOT (Proc.Closed n));
+  | term_of_fm ps vs (Proc.NClosed n) = term_of_fm ps vs (Proc.Not (Proc.Closed n));
 
 fun procedure t =
   let
diff -r 823ccd84b879 -r b4660c388e72 src/HOL/Tools/Qelim/cooper_procedure.ML
--- a/src/HOL/Tools/Qelim/cooper_procedure.ML	Fri Oct 15 22:00:28 2021 +0200
+++ b/src/HOL/Tools/Qelim/cooper_procedure.ML	Fri Oct 15 22:49:07 2021 +0200
@@ -7,7 +7,7 @@
     Neg of numa | Add of numa * numa | Sub of numa * numa | Mul of inta * numa
   datatype fm = T | F | Lt of numa | Le of numa | Gt of numa | Ge of numa |
     Eq of numa | NEq of numa | Dvd of inta * numa | NDvd of inta * numa |
-    NOT of fm | And of fm * fm | Or of fm * fm | Imp of fm * fm | Iff of fm * fm
+    Not of fm | And of fm * fm | Or of fm * fm | Imp of fm * fm | Iff of fm * fm
     | E of fm | A of fm | Closed of nat | NClosed of nat
   val pa : fm -> fm
   val nat_of_integer : int -> nat
@@ -619,7 +619,7 @@
 
 datatype fm = T | F | Lt of numa | Le of numa | Gt of numa | Ge of numa |
   Eq of numa | NEq of numa | Dvd of inta * numa | NDvd of inta * numa |
-  NOT of fm | And of fm * fm | Or of fm * fm | Imp of fm * fm | Iff of fm * fm |
+  Not of fm | And of fm * fm | Or of fm * fm | Imp of fm * fm | Iff of fm * fm |
   E of fm | A of fm | Closed of nat | NClosed of nat;
 
 fun id x = (fn xa => xa) x;
@@ -643,7 +643,7 @@
   | disjuncts (NEq v) = [NEq v]
   | disjuncts (Dvd (v, va)) = [Dvd (v, va)]
   | disjuncts (NDvd (v, va)) = [NDvd (v, va)]
-  | disjuncts (NOT v) = [NOT v]
+  | disjuncts (Not v) = [Not v]
   | disjuncts (And (v, va)) = [And (v, va)]
   | disjuncts (Imp (v, va)) = [Imp (v, va)]
   | disjuncts (Iff (v, va)) = [Iff (v, va)]
@@ -711,22 +711,22 @@
   | equal_fm (Imp (x141, x142)) (And (x121, x122)) = false
   | equal_fm (And (x121, x122)) (Or (x131, x132)) = false
   | equal_fm (Or (x131, x132)) (And (x121, x122)) = false
-  | equal_fm (NOT x11) (NClosed x19) = false
-  | equal_fm (NClosed x19) (NOT x11) = false
-  | equal_fm (NOT x11) (Closed x18) = false
-  | equal_fm (Closed x18) (NOT x11) = false
-  | equal_fm (NOT x11) (A x17) = false
-  | equal_fm (A x17) (NOT x11) = false
-  | equal_fm (NOT x11) (E x16) = false
-  | equal_fm (E x16) (NOT x11) = false
-  | equal_fm (NOT x11) (Iff (x151, x152)) = false
-  | equal_fm (Iff (x151, x152)) (NOT x11) = false
-  | equal_fm (NOT x11) (Imp (x141, x142)) = false
-  | equal_fm (Imp (x141, x142)) (NOT x11) = false
-  | equal_fm (NOT x11) (Or (x131, x132)) = false
-  | equal_fm (Or (x131, x132)) (NOT x11) = false
-  | equal_fm (NOT x11) (And (x121, x122)) = false
-  | equal_fm (And (x121, x122)) (NOT x11) = false
+  | equal_fm (Not x11) (NClosed x19) = false
+  | equal_fm (NClosed x19) (Not x11) = false
+  | equal_fm (Not x11) (Closed x18) = false
+  | equal_fm (Closed x18) (Not x11) = false
+  | equal_fm (Not x11) (A x17) = false
+  | equal_fm (A x17) (Not x11) = false
+  | equal_fm (Not x11) (E x16) = false
+  | equal_fm (E x16) (Not x11) = false
+  | equal_fm (Not x11) (Iff (x151, x152)) = false
+  | equal_fm (Iff (x151, x152)) (Not x11) = false
+  | equal_fm (Not x11) (Imp (x141, x142)) = false
+  | equal_fm (Imp (x141, x142)) (Not x11) = false
+  | equal_fm (Not x11) (Or (x131, x132)) = false
+  | equal_fm (Or (x131, x132)) (Not x11) = false
+  | equal_fm (Not x11) (And (x121, x122)) = false
+  | equal_fm (And (x121, x122)) (Not x11) = false
   | equal_fm (NDvd (x101, x102)) (NClosed x19) = false
   | equal_fm (NClosed x19) (NDvd (x101, x102)) = false
   | equal_fm (NDvd (x101, x102)) (Closed x18) = false
@@ -743,8 +743,8 @@
   | equal_fm (Or (x131, x132)) (NDvd (x101, x102)) = false
   | equal_fm (NDvd (x101, x102)) (And (x121, x122)) = false
   | equal_fm (And (x121, x122)) (NDvd (x101, x102)) = false
-  | equal_fm (NDvd (x101, x102)) (NOT x11) = false
-  | equal_fm (NOT x11) (NDvd (x101, x102)) = false
+  | equal_fm (NDvd (x101, x102)) (Not x11) = false
+  | equal_fm (Not x11) (NDvd (x101, x102)) = false
   | equal_fm (Dvd (x91, x92)) (NClosed x19) = false
   | equal_fm (NClosed x19) (Dvd (x91, x92)) = false
   | equal_fm (Dvd (x91, x92)) (Closed x18) = false
@@ -761,8 +761,8 @@
   | equal_fm (Or (x131, x132)) (Dvd (x91, x92)) = false
   | equal_fm (Dvd (x91, x92)) (And (x121, x122)) = false
   | equal_fm (And (x121, x122)) (Dvd (x91, x92)) = false
-  | equal_fm (Dvd (x91, x92)) (NOT x11) = false
-  | equal_fm (NOT x11) (Dvd (x91, x92)) = false
+  | equal_fm (Dvd (x91, x92)) (Not x11) = false
+  | equal_fm (Not x11) (Dvd (x91, x92)) = false
   | equal_fm (Dvd (x91, x92)) (NDvd (x101, x102)) = false
   | equal_fm (NDvd (x101, x102)) (Dvd (x91, x92)) = false
   | equal_fm (NEq x8) (NClosed x19) = false
@@ -781,8 +781,8 @@
   | equal_fm (Or (x131, x132)) (NEq x8) = false
   | equal_fm (NEq x8) (And (x121, x122)) = false
   | equal_fm (And (x121, x122)) (NEq x8) = false
-  | equal_fm (NEq x8) (NOT x11) = false
-  | equal_fm (NOT x11) (NEq x8) = false
+  | equal_fm (NEq x8) (Not x11) = false
+  | equal_fm (Not x11) (NEq x8) = false
   | equal_fm (NEq x8) (NDvd (x101, x102)) = false
   | equal_fm (NDvd (x101, x102)) (NEq x8) = false
   | equal_fm (NEq x8) (Dvd (x91, x92)) = false
@@ -803,8 +803,8 @@
   | equal_fm (Or (x131, x132)) (Eq x7) = false
   | equal_fm (Eq x7) (And (x121, x122)) = false
   | equal_fm (And (x121, x122)) (Eq x7) = false
-  | equal_fm (Eq x7) (NOT x11) = false
-  | equal_fm (NOT x11) (Eq x7) = false
+  | equal_fm (Eq x7) (Not x11) = false
+  | equal_fm (Not x11) (Eq x7) = false
   | equal_fm (Eq x7) (NDvd (x101, x102)) = false
   | equal_fm (NDvd (x101, x102)) (Eq x7) = false
   | equal_fm (Eq x7) (Dvd (x91, x92)) = false
@@ -827,8 +827,8 @@
   | equal_fm (Or (x131, x132)) (Ge x6) = false
   | equal_fm (Ge x6) (And (x121, x122)) = false
   | equal_fm (And (x121, x122)) (Ge x6) = false
-  | equal_fm (Ge x6) (NOT x11) = false
-  | equal_fm (NOT x11) (Ge x6) = false
+  | equal_fm (Ge x6) (Not x11) = false
+  | equal_fm (Not x11) (Ge x6) = false
   | equal_fm (Ge x6) (NDvd (x101, x102)) = false
   | equal_fm (NDvd (x101, x102)) (Ge x6) = false
   | equal_fm (Ge x6) (Dvd (x91, x92)) = false
@@ -853,8 +853,8 @@
   | equal_fm (Or (x131, x132)) (Gt x5) = false
   | equal_fm (Gt x5) (And (x121, x122)) = false
   | equal_fm (And (x121, x122)) (Gt x5) = false
-  | equal_fm (Gt x5) (NOT x11) = false
-  | equal_fm (NOT x11) (Gt x5) = false
+  | equal_fm (Gt x5) (Not x11) = false
+  | equal_fm (Not x11) (Gt x5) = false
   | equal_fm (Gt x5) (NDvd (x101, x102)) = false
   | equal_fm (NDvd (x101, x102)) (Gt x5) = false
   | equal_fm (Gt x5) (Dvd (x91, x92)) = false
@@ -881,8 +881,8 @@
   | equal_fm (Or (x131, x132)) (Le x4) = false
   | equal_fm (Le x4) (And (x121, x122)) = false
   | equal_fm (And (x121, x122)) (Le x4) = false
-  | equal_fm (Le x4) (NOT x11) = false
-  | equal_fm (NOT x11) (Le x4) = false
+  | equal_fm (Le x4) (Not x11) = false
+  | equal_fm (Not x11) (Le x4) = false
   | equal_fm (Le x4) (NDvd (x101, x102)) = false
   | equal_fm (NDvd (x101, x102)) (Le x4) = false
   | equal_fm (Le x4) (Dvd (x91, x92)) = false
@@ -911,8 +911,8 @@
   | equal_fm (Or (x131, x132)) (Lt x3) = false
   | equal_fm (Lt x3) (And (x121, x122)) = false
   | equal_fm (And (x121, x122)) (Lt x3) = false
-  | equal_fm (Lt x3) (NOT x11) = false
-  | equal_fm (NOT x11) (Lt x3) = false
+  | equal_fm (Lt x3) (Not x11) = false
+  | equal_fm (Not x11) (Lt x3) = false
   | equal_fm (Lt x3) (NDvd (x101, x102)) = false
   | equal_fm (NDvd (x101, x102)) (Lt x3) = false
   | equal_fm (Lt x3) (Dvd (x91, x92)) = false
@@ -943,8 +943,8 @@
   | equal_fm (Or (x131, x132)) F = false
   | equal_fm F (And (x121, x122)) = false
   | equal_fm (And (x121, x122)) F = false
-  | equal_fm F (NOT x11) = false
-  | equal_fm (NOT x11) F = false
+  | equal_fm F (Not x11) = false
+  | equal_fm (Not x11) F = false
   | equal_fm F (NDvd (x101, x102)) = false
   | equal_fm (NDvd (x101, x102)) F = false
   | equal_fm F (Dvd (x91, x92)) = false
@@ -977,8 +977,8 @@
   | equal_fm (Or (x131, x132)) T = false
   | equal_fm T (And (x121, x122)) = false
   | equal_fm (And (x121, x122)) T = false
-  | equal_fm T (NOT x11) = false
-  | equal_fm (NOT x11) T = false
+  | equal_fm T (Not x11) = false
+  | equal_fm (Not x11) T = false
   | equal_fm T (NDvd (x101, x102)) = false
   | equal_fm (NDvd (x101, x102)) T = false
   | equal_fm T (Dvd (x91, x92)) = false
@@ -1009,7 +1009,7 @@
     equal_fm x131 y131 andalso equal_fm x132 y132
   | equal_fm (And (x121, x122)) (And (y121, y122)) =
     equal_fm x121 y121 andalso equal_fm x122 y122
-  | equal_fm (NOT x11) (NOT y11) = equal_fm x11 y11
+  | equal_fm (Not x11) (Not y11) = equal_fm x11 y11
   | equal_fm (NDvd (x101, x102)) (NDvd (y101, y102)) =
     equal_inta x101 y101 andalso equal_numa x102 y102
   | equal_fm (Dvd (x91, x92)) (Dvd (y91, y92)) =
@@ -1030,7 +1030,7 @@
                   | Le _ => Or (f p, q) | Gt _ => Or (f p, q)
                   | Ge _ => Or (f p, q) | Eq _ => Or (f p, q)
                   | NEq _ => Or (f p, q) | Dvd (_, _) => Or (f p, q)
-                  | NDvd (_, _) => Or (f p, q) | NOT _ => Or (f p, q)
+                  | NDvd (_, _) => Or (f p, q) | Not _ => Or (f p, q)
                   | And (_, _) => Or (f p, q) | Or (_, _) => Or (f p, q)
                   | Imp (_, _) => Or (f p, q) | Iff (_, _) => Or (f p, q)
                   | E _ => Or (f p, q) | A _ => Or (f p, q)
@@ -1089,7 +1089,7 @@
   | minusinf (NEq (Mul (va, vb))) = NEq (Mul (va, vb))
   | minusinf (Dvd (v, va)) = Dvd (v, va)
   | minusinf (NDvd (v, va)) = NDvd (v, va)
-  | minusinf (NOT v) = NOT v
+  | minusinf (Not v) = Not v
   | minusinf (Imp (v, va)) = Imp (v, va)
   | minusinf (Iff (v, va)) = Iff (v, va)
   | minusinf (E v) = E v
@@ -1138,7 +1138,7 @@
   | subst0 t (NEq a) = NEq (numsubst0 t a)
   | subst0 t (Dvd (i, a)) = Dvd (i, numsubst0 t a)
   | subst0 t (NDvd (i, a)) = NDvd (i, numsubst0 t a)
-  | subst0 t (NOT p) = NOT (subst0 t p)
+  | subst0 t (Not p) = Not (subst0 t p)
   | subst0 t (And (p, q)) = And (subst0 t p, subst0 t q)
   | subst0 t (Or (p, q)) = Or (subst0 t p, subst0 t q)
   | subst0 t (Imp (p, q)) = Imp (subst0 t p, subst0 t q)
@@ -1263,25 +1263,25 @@
     else (if equal_fm p T then q
            else (if equal_fm q T then p else And (p, q))));
 
-fun nota (NOT p) = p
+fun nota (Not p) = p
   | nota T = F
   | nota F = T
-  | nota (Lt v) = NOT (Lt v)
-  | nota (Le v) = NOT (Le v)
-  | nota (Gt v) = NOT (Gt v)
-  | nota (Ge v) = NOT (Ge v)
-  | nota (Eq v) = NOT (Eq v)
-  | nota (NEq v) = NOT (NEq v)
-  | nota (Dvd (v, va)) = NOT (Dvd (v, va))
-  | nota (NDvd (v, va)) = NOT (NDvd (v, va))
-  | nota (And (v, va)) = NOT (And (v, va))
-  | nota (Or (v, va)) = NOT (Or (v, va))
-  | nota (Imp (v, va)) = NOT (Imp (v, va))
-  | nota (Iff (v, va)) = NOT (Iff (v, va))
-  | nota (E v) = NOT (E v)
-  | nota (A v) = NOT (A v)
-  | nota (Closed v) = NOT (Closed v)
-  | nota (NClosed v) = NOT (NClosed v);
+  | nota (Lt v) = Not (Lt v)
+  | nota (Le v) = Not (Le v)
+  | nota (Gt v) = Not (Gt v)
+  | nota (Ge v) = Not (Ge v)
+  | nota (Eq v) = Not (Eq v)
+  | nota (NEq v) = Not (NEq v)
+  | nota (Dvd (v, va)) = Not (Dvd (v, va))
+  | nota (NDvd (v, va)) = Not (NDvd (v, va))
+  | nota (And (v, va)) = Not (And (v, va))
+  | nota (Or (v, va)) = Not (Or (v, va))
+  | nota (Imp (v, va)) = Not (Imp (v, va))
+  | nota (Iff (v, va)) = Not (Iff (v, va))
+  | nota (E v) = Not (E v)
+  | nota (A v) = Not (A v)
+  | nota (Closed v) = Not (Closed v)
+  | nota (NClosed v) = Not (NClosed v);
 
 fun imp p q =
   (if equal_fm p F orelse equal_fm q T then T
@@ -1301,7 +1301,7 @@
   | simpfm (Or (p, q)) = disj (simpfm p) (simpfm q)
   | simpfm (Imp (p, q)) = imp (simpfm p) (simpfm q)
   | simpfm (Iff (p, q)) = iff (simpfm p) (simpfm q)
-  | simpfm (NOT p) = nota (simpfm p)
+  | simpfm (Not p) = nota (simpfm p)
   | simpfm (Lt a) =
     let
       val aa = simpnum a;
@@ -1442,7 +1442,7 @@
   | a_beta (NDvd (v, Add (vb, vc))) k = NDvd (v, Add (vb, vc))
   | a_beta (NDvd (v, Sub (vb, vc))) k = NDvd (v, Sub (vb, vc))
   | a_beta (NDvd (v, Mul (vb, vc))) k = NDvd (v, Mul (vb, vc))
-  | a_beta (NOT v) k = NOT v
+  | a_beta (Not v) k = Not v
   | a_beta (Imp (v, va)) k = Imp (v, va)
   | a_beta (Iff (v, va)) k = Iff (v, va)
   | a_beta (E v) k = E v
@@ -1515,7 +1515,7 @@
   | delta (NDvd (v, Add (vb, vc))) = one_inta
   | delta (NDvd (v, Sub (vb, vc))) = one_inta
   | delta (NDvd (v, Mul (vb, vc))) = one_inta
-  | delta (NOT v) = one_inta
+  | delta (Not v) = one_inta
   | delta (Imp (v, va)) = one_inta
   | delta (Iff (v, va)) = one_inta
   | delta (E v) = one_inta
@@ -1569,7 +1569,7 @@
   | alpha (NEq (Mul (va, vb))) = []
   | alpha (Dvd (v, va)) = []
   | alpha (NDvd (v, va)) = []
-  | alpha (NOT v) = []
+  | alpha (Not v) = []
   | alpha (Imp (v, va)) = []
   | alpha (Iff (v, va)) = []
   | alpha (E v) = []
@@ -1637,7 +1637,7 @@
   | zeta (NDvd (v, Add (vb, vc))) = one_inta
   | zeta (NDvd (v, Sub (vb, vc))) = one_inta
   | zeta (NDvd (v, Mul (vb, vc))) = one_inta
-  | zeta (NOT v) = one_inta
+  | zeta (Not v) = one_inta
   | zeta (Imp (v, va)) = one_inta
   | zeta (Iff (v, va)) = one_inta
   | zeta (E v) = one_inta
@@ -1697,7 +1697,7 @@
   | beta (NEq (Mul (va, vb))) = []
   | beta (Dvd (v, va)) = []
   | beta (NDvd (v, va)) = []
-  | beta (NOT v) = []
+  | beta (Not v) = []
   | beta (Imp (v, va)) = []
   | beta (Iff (v, va)) = []
   | beta (E v) = []
@@ -1766,7 +1766,7 @@
   | mirror (NDvd (v, Add (vb, vc))) = NDvd (v, Add (vb, vc))
   | mirror (NDvd (v, Sub (vb, vc))) = NDvd (v, Sub (vb, vc))
   | mirror (NDvd (v, Mul (vb, vc))) = NDvd (v, Mul (vb, vc))
-  | mirror (NOT v) = NOT v
+  | mirror (Not v) = Not v
   | mirror (Imp (v, va)) = Imp (v, va)
   | mirror (Iff (v, va)) = Iff (v, va)
   | mirror (E v) = E v
@@ -1848,9 +1848,9 @@
 
 fun zlfm (And (p, q)) = And (zlfm p, zlfm q)
   | zlfm (Or (p, q)) = Or (zlfm p, zlfm q)
-  | zlfm (Imp (p, q)) = Or (zlfm (NOT p), zlfm q)
+  | zlfm (Imp (p, q)) = Or (zlfm (Not p), zlfm q)
   | zlfm (Iff (p, q)) =
-    Or (And (zlfm p, zlfm q), And (zlfm (NOT p), zlfm (NOT q)))
+    Or (And (zlfm p, zlfm q), And (zlfm (Not p), zlfm (Not q)))
   | zlfm (Lt a) =
     let
       val (c, r) = zsplit0 a;
@@ -1920,28 +1920,28 @@
                       else NDvd (abs_int i,
                                   CN (zero_nat, uminus_int c, Neg r))))
            end)
-  | zlfm (NOT (And (p, q))) = Or (zlfm (NOT p), zlfm (NOT q))
-  | zlfm (NOT (Or (p, q))) = And (zlfm (NOT p), zlfm (NOT q))
-  | zlfm (NOT (Imp (p, q))) = And (zlfm p, zlfm (NOT q))
-  | zlfm (NOT (Iff (p, q))) =
-    Or (And (zlfm p, zlfm (NOT q)), And (zlfm (NOT p), zlfm q))
-  | zlfm (NOT (NOT p)) = zlfm p
-  | zlfm (NOT T) = F
-  | zlfm (NOT F) = T
-  | zlfm (NOT (Lt a)) = zlfm (Ge a)
-  | zlfm (NOT (Le a)) = zlfm (Gt a)
-  | zlfm (NOT (Gt a)) = zlfm (Le a)
-  | zlfm (NOT (Ge a)) = zlfm (Lt a)
-  | zlfm (NOT (Eq a)) = zlfm (NEq a)
-  | zlfm (NOT (NEq a)) = zlfm (Eq a)
-  | zlfm (NOT (Dvd (i, a))) = zlfm (NDvd (i, a))
-  | zlfm (NOT (NDvd (i, a))) = zlfm (Dvd (i, a))
-  | zlfm (NOT (Closed p)) = NClosed p
-  | zlfm (NOT (NClosed p)) = Closed p
+  | zlfm (Not (And (p, q))) = Or (zlfm (Not p), zlfm (Not q))
+  | zlfm (Not (Or (p, q))) = And (zlfm (Not p), zlfm (Not q))
+  | zlfm (Not (Imp (p, q))) = And (zlfm p, zlfm (Not q))
+  | zlfm (Not (Iff (p, q))) =
+    Or (And (zlfm p, zlfm (Not q)), And (zlfm (Not p), zlfm q))
+  | zlfm (Not (Not p)) = zlfm p
+  | zlfm (Not T) = F
+  | zlfm (Not F) = T
+  | zlfm (Not (Lt a)) = zlfm (Ge a)
+  | zlfm (Not (Le a)) = zlfm (Gt a)
+  | zlfm (Not (Gt a)) = zlfm (Le a)
+  | zlfm (Not (Ge a)) = zlfm (Lt a)
+  | zlfm (Not (Eq a)) = zlfm (NEq a)
+  | zlfm (Not (NEq a)) = zlfm (Eq a)
+  | zlfm (Not (Dvd (i, a))) = zlfm (NDvd (i, a))
+  | zlfm (Not (NDvd (i, a))) = zlfm (Dvd (i, a))
+  | zlfm (Not (Closed p)) = NClosed p
+  | zlfm (Not (NClosed p)) = Closed p
   | zlfm T = T
   | zlfm F = F
-  | zlfm (NOT (E va)) = NOT (E va)
-  | zlfm (NOT (A va)) = NOT (A va)
+  | zlfm (Not (E va)) = Not (E va)
+  | zlfm (Not (A va)) = Not (A va)
   | zlfm (E v) = E v
   | zlfm (A v) = A v
   | zlfm (Closed v) = Closed v
@@ -1976,7 +1976,7 @@
   | decr (NEq a) = NEq (decrnum a)
   | decr (Dvd (i, a)) = Dvd (i, decrnum a)
   | decr (NDvd (i, a)) = NDvd (i, decrnum a)
-  | decr (NOT p) = NOT (decr p)
+  | decr (Not p) = Not (decr p)
   | decr (And (p, q)) = And (decr p, decr q)
   | decr (Or (p, q)) = Or (decr p, decr q)
   | decr (Imp (p, q)) = Imp (decr p, decr q)
@@ -2014,8 +2014,8 @@
   end;
 
 fun qelim (E p) = (fn qe => dj qe (qelim p qe))
-  | qelim (A p) = (fn qe => nota (qe (qelim (NOT p) qe)))
-  | qelim (NOT p) = (fn qe => nota (qelim p qe))
+  | qelim (A p) = (fn qe => nota (qe (qelim (Not p) qe)))
+  | qelim (Not p) = (fn qe => nota (qelim p qe))
   | qelim (And (p, q)) = (fn qe => conj (qelim p qe) (qelim q qe))
   | qelim (Or (p, q)) = (fn qe => disj (qelim p qe) (qelim q qe))
   | qelim (Imp (p, q)) = (fn qe => imp (qelim p qe) (qelim q qe))
@@ -2036,13 +2036,13 @@
 fun prep (E T) = T
   | prep (E F) = F
   | prep (E (Or (p, q))) = Or (prep (E p), prep (E q))
-  | prep (E (Imp (p, q))) = Or (prep (E (NOT p)), prep (E q))
+  | prep (E (Imp (p, q))) = Or (prep (E (Not p)), prep (E q))
   | prep (E (Iff (p, q))) =
-    Or (prep (E (And (p, q))), prep (E (And (NOT p, NOT q))))
-  | prep (E (NOT (And (p, q)))) = Or (prep (E (NOT p)), prep (E (NOT q)))
-  | prep (E (NOT (Imp (p, q)))) = prep (E (And (p, NOT q)))
-  | prep (E (NOT (Iff (p, q)))) =
-    Or (prep (E (And (p, NOT q))), prep (E (And (NOT p, q))))
+    Or (prep (E (And (p, q))), prep (E (And (Not p, Not q))))
+  | prep (E (Not (And (p, q)))) = Or (prep (E (Not p)), prep (E (Not q)))
+  | prep (E (Not (Imp (p, q)))) = prep (E (And (p, Not q)))
+  | prep (E (Not (Iff (p, q)))) =
+    Or (prep (E (And (p, Not q))), prep (E (And (Not p, q))))
   | prep (E (Lt v)) = E (prep (Lt v))
   | prep (E (Le v)) = E (prep (Le v))
   | prep (E (Gt v)) = E (prep (Gt v))
@@ -2051,69 +2051,69 @@
   | prep (E (NEq v)) = E (prep (NEq v))
   | prep (E (Dvd (v, va))) = E (prep (Dvd (v, va)))
   | prep (E (NDvd (v, va))) = E (prep (NDvd (v, va)))
-  | prep (E (NOT T)) = E (prep (NOT T))
-  | prep (E (NOT F)) = E (prep (NOT F))
-  | prep (E (NOT (Lt va))) = E (prep (NOT (Lt va)))
-  | prep (E (NOT (Le va))) = E (prep (NOT (Le va)))
-  | prep (E (NOT (Gt va))) = E (prep (NOT (Gt va)))
-  | prep (E (NOT (Ge va))) = E (prep (NOT (Ge va)))
-  | prep (E (NOT (Eq va))) = E (prep (NOT (Eq va)))
-  | prep (E (NOT (NEq va))) = E (prep (NOT (NEq va)))
-  | prep (E (NOT (Dvd (va, vb)))) = E (prep (NOT (Dvd (va, vb))))
-  | prep (E (NOT (NDvd (va, vb)))) = E (prep (NOT (NDvd (va, vb))))
-  | prep (E (NOT (NOT va))) = E (prep (NOT (NOT va)))
-  | prep (E (NOT (Or (va, vb)))) = E (prep (NOT (Or (va, vb))))
-  | prep (E (NOT (E va))) = E (prep (NOT (E va)))
-  | prep (E (NOT (A va))) = E (prep (NOT (A va)))
-  | prep (E (NOT (Closed va))) = E (prep (NOT (Closed va)))
-  | prep (E (NOT (NClosed va))) = E (prep (NOT (NClosed va)))
+  | prep (E (Not T)) = E (prep (Not T))
+  | prep (E (Not F)) = E (prep (Not F))
+  | prep (E (Not (Lt va))) = E (prep (Not (Lt va)))
+  | prep (E (Not (Le va))) = E (prep (Not (Le va)))
+  | prep (E (Not (Gt va))) = E (prep (Not (Gt va)))
+  | prep (E (Not (Ge va))) = E (prep (Not (Ge va)))
+  | prep (E (Not (Eq va))) = E (prep (Not (Eq va)))
+  | prep (E (Not (NEq va))) = E (prep (Not (NEq va)))
+  | prep (E (Not (Dvd (va, vb)))) = E (prep (Not (Dvd (va, vb))))
+  | prep (E (Not (NDvd (va, vb)))) = E (prep (Not (NDvd (va, vb))))
+  | prep (E (Not (Not va))) = E (prep (Not (Not va)))
+  | prep (E (Not (Or (va, vb)))) = E (prep (Not (Or (va, vb))))
+  | prep (E (Not (E va))) = E (prep (Not (E va)))
+  | prep (E (Not (A va))) = E (prep (Not (A va)))
+  | prep (E (Not (Closed va))) = E (prep (Not (Closed va)))
+  | prep (E (Not (NClosed va))) = E (prep (Not (NClosed va)))
   | prep (E (And (v, va))) = E (prep (And (v, va)))
   | prep (E (E v)) = E (prep (E v))
   | prep (E (A v)) = E (prep (A v))
   | prep (E (Closed v)) = E (prep (Closed v))
   | prep (E (NClosed v)) = E (prep (NClosed v))
   | prep (A (And (p, q))) = And (prep (A p), prep (A q))
-  | prep (A T) = prep (NOT (E (NOT T)))
-  | prep (A F) = prep (NOT (E (NOT F)))
-  | prep (A (Lt v)) = prep (NOT (E (NOT (Lt v))))
-  | prep (A (Le v)) = prep (NOT (E (NOT (Le v))))
-  | prep (A (Gt v)) = prep (NOT (E (NOT (Gt v))))
-  | prep (A (Ge v)) = prep (NOT (E (NOT (Ge v))))
-  | prep (A (Eq v)) = prep (NOT (E (NOT (Eq v))))
-  | prep (A (NEq v)) = prep (NOT (E (NOT (NEq v))))
-  | prep (A (Dvd (v, va))) = prep (NOT (E (NOT (Dvd (v, va)))))
-  | prep (A (NDvd (v, va))) = prep (NOT (E (NOT (NDvd (v, va)))))
-  | prep (A (NOT v)) = prep (NOT (E (NOT (NOT v))))
-  | prep (A (Or (v, va))) = prep (NOT (E (NOT (Or (v, va)))))
-  | prep (A (Imp (v, va))) = prep (NOT (E (NOT (Imp (v, va)))))
-  | prep (A (Iff (v, va))) = prep (NOT (E (NOT (Iff (v, va)))))
-  | prep (A (E v)) = prep (NOT (E (NOT (E v))))
-  | prep (A (A v)) = prep (NOT (E (NOT (A v))))
-  | prep (A (Closed v)) = prep (NOT (E (NOT (Closed v))))
-  | prep (A (NClosed v)) = prep (NOT (E (NOT (NClosed v))))
-  | prep (NOT (NOT p)) = prep p
-  | prep (NOT (And (p, q))) = Or (prep (NOT p), prep (NOT q))
-  | prep (NOT (A p)) = prep (E (NOT p))
-  | prep (NOT (Or (p, q))) = And (prep (NOT p), prep (NOT q))
-  | prep (NOT (Imp (p, q))) = And (prep p, prep (NOT q))
-  | prep (NOT (Iff (p, q))) = Or (prep (And (p, NOT q)), prep (And (NOT p, q)))
-  | prep (NOT T) = NOT (prep T)
-  | prep (NOT F) = NOT (prep F)
-  | prep (NOT (Lt v)) = NOT (prep (Lt v))
-  | prep (NOT (Le v)) = NOT (prep (Le v))
-  | prep (NOT (Gt v)) = NOT (prep (Gt v))
-  | prep (NOT (Ge v)) = NOT (prep (Ge v))
-  | prep (NOT (Eq v)) = NOT (prep (Eq v))
-  | prep (NOT (NEq v)) = NOT (prep (NEq v))
-  | prep (NOT (Dvd (v, va))) = NOT (prep (Dvd (v, va)))
-  | prep (NOT (NDvd (v, va))) = NOT (prep (NDvd (v, va)))
-  | prep (NOT (E v)) = NOT (prep (E v))
-  | prep (NOT (Closed v)) = NOT (prep (Closed v))
-  | prep (NOT (NClosed v)) = NOT (prep (NClosed v))
+  | prep (A T) = prep (Not (E (Not T)))
+  | prep (A F) = prep (Not (E (Not F)))
+  | prep (A (Lt v)) = prep (Not (E (Not (Lt v))))
+  | prep (A (Le v)) = prep (Not (E (Not (Le v))))
+  | prep (A (Gt v)) = prep (Not (E (Not (Gt v))))
+  | prep (A (Ge v)) = prep (Not (E (Not (Ge v))))
+  | prep (A (Eq v)) = prep (Not (E (Not (Eq v))))
+  | prep (A (NEq v)) = prep (Not (E (Not (NEq v))))
+  | prep (A (Dvd (v, va))) = prep (Not (E (Not (Dvd (v, va)))))
+  | prep (A (NDvd (v, va))) = prep (Not (E (Not (NDvd (v, va)))))
+  | prep (A (Not v)) = prep (Not (E (Not (Not v))))
+  | prep (A (Or (v, va))) = prep (Not (E (Not (Or (v, va)))))
+  | prep (A (Imp (v, va))) = prep (Not (E (Not (Imp (v, va)))))
+  | prep (A (Iff (v, va))) = prep (Not (E (Not (Iff (v, va)))))
+  | prep (A (E v)) = prep (Not (E (Not (E v))))
+  | prep (A (A v)) = prep (Not (E (Not (A v))))
+  | prep (A (Closed v)) = prep (Not (E (Not (Closed v))))
+  | prep (A (NClosed v)) = prep (Not (E (Not (NClosed v))))
+  | prep (Not (Not p)) = prep p
+  | prep (Not (And (p, q))) = Or (prep (Not p), prep (Not q))
+  | prep (Not (A p)) = prep (E (Not p))
+  | prep (Not (Or (p, q))) = And (prep (Not p), prep (Not q))
+  | prep (Not (Imp (p, q))) = And (prep p, prep (Not q))
+  | prep (Not (Iff (p, q))) = Or (prep (And (p, Not q)), prep (And (Not p, q)))
+  | prep (Not T) = Not (prep T)
+  | prep (Not F) = Not (prep F)
+  | prep (Not (Lt v)) = Not (prep (Lt v))
+  | prep (Not (Le v)) = Not (prep (Le v))
+  | prep (Not (Gt v)) = Not (prep (Gt v))
+  | prep (Not (Ge v)) = Not (prep (Ge v))
+  | prep (Not (Eq v)) = Not (prep (Eq v))
+  | prep (Not (NEq v)) = Not (prep (NEq v))
+  | prep (Not (Dvd (v, va))) = Not (prep (Dvd (v, va)))
+  | prep (Not (NDvd (v, va))) = Not (prep (NDvd (v, va)))
+  | prep (Not (E v)) = Not (prep (E v))
+  | prep (Not (Closed v)) = Not (prep (Closed v))
+  | prep (Not (NClosed v)) = Not (prep (NClosed v))
   | prep (Or (p, q)) = Or (prep p, prep q)
   | prep (And (p, q)) = And (prep p, prep q)
-  | prep (Imp (p, q)) = prep (Or (NOT p, q))
-  | prep (Iff (p, q)) = Or (prep (And (p, q)), prep (And (NOT p, NOT q)))
+  | prep (Imp (p, q)) = prep (Or (Not p, q))
+  | prep (Iff (p, q)) = Or (prep (And (p, q)), prep (And (Not p, Not q)))
   | prep T = T
   | prep F = F
   | prep (Lt v) = Lt v