src/HOL/Import/HOL/HOL4Real.thy
changeset 15013 34264f5e4691
parent 14847 44d92c12b255
child 15071 b65fc0787fbe
--- a/src/HOL/Import/HOL/HOL4Real.thy	Wed Jun 30 14:04:58 2004 +0200
+++ b/src/HOL/Import/HOL/HOL4Real.thy	Thu Jul 01 12:29:53 2004 +0200
@@ -1916,13 +1916,13 @@
                ((op *::nat => nat => nat)
                  ((number_of::bin => nat)
                    ((op BIT::bin => bool => bin)
-                     ((op BIT::bin => bool => bin) (bin.Pls::bin)
+                     ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
                        (True::bool))
                      (False::bool)))
                  n)
                ((number_of::bin => nat)
                  ((op BIT::bin => bool => bin)
-                   ((op BIT::bin => bool => bin) (bin.Pls::bin)
+                   ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
                      (True::bool))
                    (False::bool))))
              f)
@@ -1958,7 +1958,7 @@
                              ((number_of::bin => nat)
                                ((op BIT::bin => bool => bin)
                                  ((op BIT::bin => bool => bin)
-                                   (bin.Pls::bin) (True::bool))
+                                   (Numeral.Pls::bin) (True::bool))
                                  (False::bool)))
                              d)))
                       (f ((op +::nat => nat => nat) n
@@ -1967,7 +1967,7 @@
                                ((number_of::bin => nat)
                                  ((op BIT::bin => bool => bin)
                                    ((op BIT::bin => bool => bin)
-                                     (bin.Pls::bin) (True::bool))
+                                     (Numeral.Pls::bin) (True::bool))
                                    (False::bool)))
                                d)
                              (1::nat))))))))
@@ -2825,7 +2825,7 @@
           ((op ^::real => nat => real) ((inverse::real => real) x)
             ((number_of::bin => nat)
               ((op BIT::bin => bool => bin)
-                ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+                ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
                 (False::bool)))))
         x))"
   by (import lim DIFF_XM1)
@@ -2848,7 +2848,7 @@
                       ((op ^::real => nat => real) (f x)
                         ((number_of::bin => nat)
                           ((op BIT::bin => bool => bin)
-                            ((op BIT::bin => bool => bin) (bin.Pls::bin)
+                            ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
                               (True::bool))
                             (False::bool))))))
                   x))))"
@@ -2886,7 +2886,7 @@
                                 ((number_of::bin => nat)
                                   ((op BIT::bin => bool => bin)
                                     ((op BIT::bin => bool => bin)
-(bin.Pls::bin) (True::bool))
+(Numeral.Pls::bin) (True::bool))
                                     (False::bool)))))
                             x))))))"
   by (import lim DIFF_DIV)
@@ -3869,7 +3869,7 @@
   ((op -::nat => nat => nat) n
     ((number_of::bin => nat)
       ((op BIT::bin => bool => bin)
-        ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+        ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
         (False::bool))))
   p)
 q)))))))))))"
@@ -3917,7 +3917,7 @@
                                  ((number_of::bin => nat)
                                    ((op BIT::bin => bool => bin)
                                      ((op BIT::bin => bool => bin)
- (bin.Pls::bin) (True::bool))
+ (Numeral.Pls::bin) (True::bool))
                                      (False::bool)))))
                              ((abs::real => real) h)))))))))"
   by (import powser TERMDIFF_LEMMA3)
@@ -4112,7 +4112,7 @@
          ((op ^::real => nat => real) (f x)
            ((number_of::bin => nat)
              ((op BIT::bin => bool => bin)
-               ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+               ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
                (False::bool))))))
      x))
  ((op &::bool => bool => bool)
@@ -4133,7 +4133,7 @@
          ((op ^::real => nat => real) (g x)
            ((number_of::bin => nat)
              ((op BIT::bin => bool => bin)
-               ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+               ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
                (False::bool)))))
        x))
    ((op &::bool => bool => bool)
@@ -4652,7 +4652,7 @@
         ((op ^::real => nat => real) ((sqrt::real => real) x)
           ((number_of::bin => nat)
             ((op BIT::bin => bool => bin)
-              ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+              ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
               (False::bool))))
         x))"
   by (import transc SQRT_POW_2)
@@ -4664,7 +4664,7 @@
      ((op ^::real => nat => real) x
        ((number_of::bin => nat)
          ((op BIT::bin => bool => bin)
-           ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+           ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
            (False::bool)))))
    x)"
   by (import transc POW_2_SQRT)
@@ -4682,7 +4682,7 @@
                  ((op ^::real => nat => real) xa
                    ((number_of::bin => nat)
                      ((op BIT::bin => bool => bin)
-                       ((op BIT::bin => bool => bin) (bin.Pls::bin)
+                       ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
                          (True::bool))
                        (False::bool))))
                  x)))
@@ -4746,18 +4746,18 @@
           ((op ^::real => nat => real)
             ((number_of::bin => real)
               ((op BIT::bin => bool => bin)
-                ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+                ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
                 (False::bool)))
             n))
         ((op ^::real => nat => real)
           ((number_of::bin => real)
             ((op BIT::bin => bool => bin)
-              ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+              ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
               (False::bool)))
           ((op div::nat => nat => nat) n
             ((number_of::bin => nat)
               ((op BIT::bin => bool => bin)
-                ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+                ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
                 (False::bool)))))))"
   by (import transc SQRT_EVEN_POW2)
 
@@ -4780,7 +4780,7 @@
                ((op ^::real => nat => real) x
                  ((number_of::bin => nat)
                    ((op BIT::bin => bool => bin)
-                     ((op BIT::bin => bool => bin) (bin.Pls::bin)
+                     ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
                        (True::bool))
                      (False::bool))))
                y)
@@ -4848,7 +4848,7 @@
         ((op <::real => real => bool) x
           ((number_of::bin => real)
             ((op BIT::bin => bool => bin)
-              ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+              ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
               (False::bool)))))
       ((op <::real => real => bool) (0::real) ((sin::real => real) x)))"
   by (import transc SIN_POS)
@@ -4923,7 +4923,7 @@
           ((op /::real => real => real) (pi::real)
             ((number_of::bin => real)
               ((op BIT::bin => bool => bin)
-                ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+                ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
                 (False::bool))))))
       ((op <::real => real => bool) (0::real) ((sin::real => real) x)))"
   by (import transc SIN_POS_PI2)
@@ -4937,7 +4937,7 @@
           ((op /::real => real => real) (pi::real)
             ((number_of::bin => real)
               ((op BIT::bin => bool => bin)
-                ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+                ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
                 (False::bool))))))
       ((op <::real => real => bool) (0::real) ((cos::real => real) x)))"
   by (import transc COS_POS_PI2)
@@ -4951,14 +4951,14 @@
             ((op /::real => real => real) (pi::real)
               ((number_of::bin => real)
                 ((op BIT::bin => bool => bin)
-                  ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+                  ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
                   (False::bool)))))
           x)
         ((op <::real => real => bool) x
           ((op /::real => real => real) (pi::real)
             ((number_of::bin => real)
               ((op BIT::bin => bool => bin)
-                ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+                ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
                 (False::bool))))))
       ((op <::real => real => bool) (0::real) ((cos::real => real) x)))"
   by (import transc COS_POS_PI)
@@ -4981,7 +4981,7 @@
           ((op /::real => real => real) (pi::real)
             ((number_of::bin => real)
               ((op BIT::bin => bool => bin)
-                ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+                ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
                 (False::bool))))))
       ((op <=::real => real => bool) (0::real) ((cos::real => real) x)))"
   by (import transc COS_POS_PI2_LE)
@@ -4995,14 +4995,14 @@
             ((op /::real => real => real) (pi::real)
               ((number_of::bin => real)
                 ((op BIT::bin => bool => bin)
-                  ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+                  ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
                   (False::bool)))))
           x)
         ((op <=::real => real => bool) x
           ((op /::real => real => real) (pi::real)
             ((number_of::bin => real)
               ((op BIT::bin => bool => bin)
-                ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+                ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
                 (False::bool))))))
       ((op <=::real => real => bool) (0::real) ((cos::real => real) x)))"
   by (import transc COS_POS_PI_LE)
@@ -5016,7 +5016,7 @@
           ((op /::real => real => real) (pi::real)
             ((number_of::bin => real)
               ((op BIT::bin => bool => bin)
-                ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+                ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
                 (False::bool))))))
       ((op <=::real => real => bool) (0::real) ((sin::real => real) x)))"
   by (import transc SIN_POS_PI2_LE)
@@ -5059,7 +5059,7 @@
                  ((op /::real => real => real) (pi::real)
                    ((number_of::bin => real)
                      ((op BIT::bin => bool => bin)
-                       ((op BIT::bin => bool => bin) (bin.Pls::bin)
+                       ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
                          (True::bool))
                        (False::bool)))))
                x)
@@ -5068,7 +5068,7 @@
                  ((op /::real => real => real) (pi::real)
                    ((number_of::bin => real)
                      ((op BIT::bin => bool => bin)
-                       ((op BIT::bin => bool => bin) (bin.Pls::bin)
+                       ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
                          (True::bool))
                        (False::bool)))))
                ((op =::real => real => bool) ((sin::real => real) x) y)))))"
@@ -5089,7 +5089,7 @@
                  ((op /::real => real => real) (pi::real)
                    ((number_of::bin => real)
                      ((op BIT::bin => bool => bin)
-                       ((op BIT::bin => bool => bin) (bin.Pls::bin)
+                       ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
                          (True::bool))
                        (False::bool)))))))))"
   by (import transc COS_ZERO_LEMMA)
@@ -5108,7 +5108,7 @@
                  ((op /::real => real => real) (pi::real)
                    ((number_of::bin => real)
                      ((op BIT::bin => bool => bin)
-                       ((op BIT::bin => bool => bin) (bin.Pls::bin)
+                       ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
                          (True::bool))
                        (False::bool)))))))))"
   by (import transc SIN_ZERO_LEMMA)
@@ -5186,7 +5186,7 @@
               ((op *::real => real => real)
                 ((number_of::bin => real)
                   ((op BIT::bin => bool => bin)
-                    ((op BIT::bin => bool => bin) (bin.Pls::bin)
+                    ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
                       (True::bool))
                     (False::bool)))
                 x))
@@ -5196,21 +5196,21 @@
           ((op *::real => real => real)
             ((number_of::bin => real)
               ((op BIT::bin => bool => bin)
-                ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+                ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
                 (False::bool)))
             x))
         ((op /::real => real => real)
           ((op *::real => real => real)
             ((number_of::bin => real)
               ((op BIT::bin => bool => bin)
-                ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+                ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
                 (False::bool)))
             ((tan::real => real) x))
           ((op -::real => real => real) (1::real)
             ((op ^::real => nat => real) ((tan::real => real) x)
               ((number_of::bin => nat)
                 ((op BIT::bin => bool => bin)
-                  ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+                  ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
                   (False::bool))))))))"
   by (import transc TAN_DOUBLE)
 
@@ -5223,7 +5223,7 @@
           ((op /::real => real => real) (pi::real)
             ((number_of::bin => real)
               ((op BIT::bin => bool => bin)
-                ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+                ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
                 (False::bool))))))
       ((op <::real => real => bool) (0::real) ((tan::real => real) x)))"
   by (import transc TAN_POS_PI2)
@@ -5238,7 +5238,7 @@
           ((op ^::real => nat => real) ((cos::real => real) x)
             ((number_of::bin => nat)
               ((op BIT::bin => bool => bin)
-                ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+                ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
                 (False::bool)))))
         x))"
   by (import transc DIFF_TAN)
@@ -5256,7 +5256,7 @@
                  ((op /::real => real => real) (pi::real)
                    ((number_of::bin => real)
                      ((op BIT::bin => bool => bin)
-                       ((op BIT::bin => bool => bin) (bin.Pls::bin)
+                       ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
                          (True::bool))
                        (False::bool)))))
                ((op <::real => real => bool) y ((tan::real => real) x))))))"
@@ -5275,7 +5275,7 @@
                  ((op /::real => real => real) (pi::real)
                    ((number_of::bin => real)
                      ((op BIT::bin => bool => bin)
-                       ((op BIT::bin => bool => bin) (bin.Pls::bin)
+                       ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
                          (True::bool))
                        (False::bool)))))
                ((op =::real => real => bool) ((tan::real => real) x) y)))))"
@@ -5317,7 +5317,7 @@
             ((op /::real => real => real) (pi::real)
               ((number_of::bin => real)
                 ((op BIT::bin => bool => bin)
-                  ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+                  ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
                   (False::bool)))))
           ((asn::real => real) y))
         ((op &::bool => bool => bool)
@@ -5325,7 +5325,7 @@
             ((op /::real => real => real) (pi::real)
               ((number_of::bin => real)
                 ((op BIT::bin => bool => bin)
-                  ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+                  ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
                   (False::bool)))))
           ((op =::real => real => bool)
             ((sin::real => real) ((asn::real => real) y)) y))))"
@@ -5353,14 +5353,14 @@
             ((op /::real => real => real) (pi::real)
               ((number_of::bin => real)
                 ((op BIT::bin => bool => bin)
-                  ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+                  ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
                   (False::bool)))))
           ((asn::real => real) y))
         ((op <=::real => real => bool) ((asn::real => real) y)
           ((op /::real => real => real) (pi::real)
             ((number_of::bin => real)
               ((op BIT::bin => bool => bin)
-                ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+                ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
                 (False::bool)))))))"
   by (import transc ASN_BOUNDS)
 
@@ -5376,14 +5376,14 @@
             ((op /::real => real => real) (pi::real)
               ((number_of::bin => real)
                 ((op BIT::bin => bool => bin)
-                  ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+                  ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
                   (False::bool)))))
           ((asn::real => real) y))
         ((op <::real => real => bool) ((asn::real => real) y)
           ((op /::real => real => real) (pi::real)
             ((number_of::bin => real)
               ((op BIT::bin => bool => bin)
-                ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+                ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
                 (False::bool)))))))"
   by (import transc ASN_BOUNDS_LT)
 
@@ -5396,14 +5396,14 @@
             ((op /::real => real => real) (pi::real)
               ((number_of::bin => real)
                 ((op BIT::bin => bool => bin)
-                  ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+                  ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
                   (False::bool)))))
           x)
         ((op <=::real => real => bool) x
           ((op /::real => real => real) (pi::real)
             ((number_of::bin => real)
               ((op BIT::bin => bool => bin)
-                ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+                ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
                 (False::bool))))))
       ((op =::real => real => bool)
         ((asn::real => real) ((sin::real => real) x)) x))"
@@ -5483,14 +5483,14 @@
             ((op /::real => real => real) (pi::real)
               ((number_of::bin => real)
                 ((op BIT::bin => bool => bin)
-                  ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+                  ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
                   (False::bool)))))
           x)
         ((op <::real => real => bool) x
           ((op /::real => real => real) (pi::real)
             ((number_of::bin => real)
               ((op BIT::bin => bool => bin)
-                ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+                ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
                 (False::bool))))))
       ((op =::real => real => bool)
         ((atn::real => real) ((tan::real => real) x)) x))"
@@ -5506,13 +5506,13 @@
           ((op ^::real => nat => real) ((tan::real => real) x)
             ((number_of::bin => nat)
               ((op BIT::bin => bool => bin)
-                ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+                ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
                 (False::bool)))))
         ((op ^::real => nat => real)
           ((inverse::real => real) ((cos::real => real) x))
           ((number_of::bin => nat)
             ((op BIT::bin => bool => bin)
-              ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+              ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
               (False::bool))))))"
   by (import transc TAN_SEC)
 
@@ -5528,7 +5528,7 @@
             ((op ^::real => nat => real) ((cos::real => real) x)
               ((number_of::bin => nat)
                 ((op BIT::bin => bool => bin)
-                  ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+                  ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
                   (False::bool))))))))"
   by (import transc SIN_COS_SQ)
 
@@ -5541,14 +5541,14 @@
             ((op /::real => real => real) (pi::real)
               ((number_of::bin => real)
                 ((op BIT::bin => bool => bin)
-                  ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+                  ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
                   (False::bool)))))
           x)
         ((op <=::real => real => bool) x
           ((op /::real => real => real) (pi::real)
             ((number_of::bin => real)
               ((op BIT::bin => bool => bin)
-                ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+                ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
                 (False::bool))))))
       ((op =::real => real => bool) ((cos::real => real) x)
         ((sqrt::real => real)
@@ -5556,7 +5556,7 @@
             ((op ^::real => nat => real) ((sin::real => real) x)
               ((number_of::bin => nat)
                 ((op BIT::bin => bool => bin)
-                  ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+                  ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
                   (False::bool))))))))"
   by (import transc COS_SIN_SQ)
 
@@ -5595,7 +5595,7 @@
             ((op ^::real => nat => real) ((sin::real => real) x)
               ((number_of::bin => nat)
                 ((op BIT::bin => bool => bin)
-                  ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+                  ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
                   (False::bool))))))))"
   by (import transc COS_SIN_SQRT)
 
@@ -5609,7 +5609,7 @@
             ((op ^::real => nat => real) ((cos::real => real) x)
               ((number_of::bin => nat)
                 ((op BIT::bin => bool => bin)
-                  ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+                  ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
                   (False::bool))))))))"
   by (import transc SIN_COS_SQRT)
 
@@ -5646,7 +5646,7 @@
               ((op ^::real => nat => real) x
                 ((number_of::bin => nat)
                   ((op BIT::bin => bool => bin)
-                    ((op BIT::bin => bool => bin) (bin.Pls::bin)
+                    ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
                       (True::bool))
                     (False::bool)))))))
         x))"
@@ -5679,7 +5679,7 @@
                 ((op ^::real => nat => real) x
                   ((number_of::bin => nat)
                     ((op BIT::bin => bool => bin)
-                      ((op BIT::bin => bool => bin) (bin.Pls::bin)
+                      ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
                         (True::bool))
                       (False::bool))))))))
         x))"