src/HOL/Import/HOL/HOL4Real.thy
changeset 15071 b65fc0787fbe
parent 15013 34264f5e4691
child 15647 b1f486a9c56b
--- a/src/HOL/Import/HOL/HOL4Real.thy	Wed Jul 21 08:35:29 2004 +0200
+++ b/src/HOL/Import/HOL/HOL4Real.thy	Wed Jul 21 16:35:38 2004 +0200
@@ -2825,7 +2825,8 @@
           ((op ^::real => nat => real) ((inverse::real => real) x)
             ((number_of::bin => nat)
               ((op BIT::bin => bool => bin)
-                ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
+                ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
+                  (True::bool))
                 (False::bool)))))
         x))"
   by (import lim DIFF_XM1)
@@ -4112,7 +4113,8 @@
          ((op ^::real => nat => real) (f x)
            ((number_of::bin => nat)
              ((op BIT::bin => bool => bin)
-               ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
+               ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
+                 (True::bool))
                (False::bool))))))
      x))
  ((op &::bool => bool => bool)
@@ -4133,7 +4135,8 @@
          ((op ^::real => nat => real) (g x)
            ((number_of::bin => nat)
              ((op BIT::bin => bool => bin)
-               ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
+               ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
+                 (True::bool))
                (False::bool)))))
        x))
    ((op &::bool => bool => bool)
@@ -4746,7 +4749,8 @@
           ((op ^::real => nat => real)
             ((number_of::bin => real)
               ((op BIT::bin => bool => bin)
-                ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
+                ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
+                  (True::bool))
                 (False::bool)))
             n))
         ((op ^::real => nat => real)
@@ -4757,7 +4761,8 @@
           ((op div::nat => nat => nat) n
             ((number_of::bin => nat)
               ((op BIT::bin => bool => bin)
-                ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
+                ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
+                  (True::bool))
                 (False::bool)))))))"
   by (import transc SQRT_EVEN_POW2)
 
@@ -4923,7 +4928,8 @@
           ((op /::real => real => real) (pi::real)
             ((number_of::bin => real)
               ((op BIT::bin => bool => bin)
-                ((op BIT::bin => bool => bin) (Numeral.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 +4943,8 @@
           ((op /::real => real => real) (pi::real)
             ((number_of::bin => real)
               ((op BIT::bin => bool => bin)
-                ((op BIT::bin => bool => bin) (Numeral.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 +4958,16 @@
             ((op /::real => real => real) (pi::real)
               ((number_of::bin => real)
                 ((op BIT::bin => bool => bin)
-                  ((op BIT::bin => bool => bin) (Numeral.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) (Numeral.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 +4990,8 @@
           ((op /::real => real => real) (pi::real)
             ((number_of::bin => real)
               ((op BIT::bin => bool => bin)
-                ((op BIT::bin => bool => bin) (Numeral.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 +5005,16 @@
             ((op /::real => real => real) (pi::real)
               ((number_of::bin => real)
                 ((op BIT::bin => bool => bin)
-                  ((op BIT::bin => bool => bin) (Numeral.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) (Numeral.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 +5028,8 @@
           ((op /::real => real => real) (pi::real)
             ((number_of::bin => real)
               ((op BIT::bin => bool => bin)
-                ((op BIT::bin => bool => bin) (Numeral.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)
@@ -5196,21 +5209,24 @@
           ((op *::real => real => real)
             ((number_of::bin => real)
               ((op BIT::bin => bool => bin)
-                ((op BIT::bin => bool => bin) (Numeral.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) (Numeral.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) (Numeral.Pls::bin) (True::bool))
+                  ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
+                    (True::bool))
                   (False::bool))))))))"
   by (import transc TAN_DOUBLE)
 
@@ -5223,7 +5239,8 @@
           ((op /::real => real => real) (pi::real)
             ((number_of::bin => real)
               ((op BIT::bin => bool => bin)
-                ((op BIT::bin => bool => bin) (Numeral.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 +5255,8 @@
           ((op ^::real => nat => real) ((cos::real => real) x)
             ((number_of::bin => nat)
               ((op BIT::bin => bool => bin)
-                ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
+                ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
+                  (True::bool))
                 (False::bool)))))
         x))"
   by (import transc DIFF_TAN)
@@ -5317,7 +5335,8 @@
             ((op /::real => real => real) (pi::real)
               ((number_of::bin => real)
                 ((op BIT::bin => bool => bin)
-                  ((op BIT::bin => bool => bin) (Numeral.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 +5344,8 @@
             ((op /::real => real => real) (pi::real)
               ((number_of::bin => real)
                 ((op BIT::bin => bool => bin)
-                  ((op BIT::bin => bool => bin) (Numeral.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 +5373,16 @@
             ((op /::real => real => real) (pi::real)
               ((number_of::bin => real)
                 ((op BIT::bin => bool => bin)
-                  ((op BIT::bin => bool => bin) (Numeral.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) (Numeral.Pls::bin) (True::bool))
+                ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
+                  (True::bool))
                 (False::bool)))))))"
   by (import transc ASN_BOUNDS)
 
@@ -5376,14 +5398,16 @@
             ((op /::real => real => real) (pi::real)
               ((number_of::bin => real)
                 ((op BIT::bin => bool => bin)
-                  ((op BIT::bin => bool => bin) (Numeral.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) (Numeral.Pls::bin) (True::bool))
+                ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
+                  (True::bool))
                 (False::bool)))))))"
   by (import transc ASN_BOUNDS_LT)
 
@@ -5396,14 +5420,16 @@
             ((op /::real => real => real) (pi::real)
               ((number_of::bin => real)
                 ((op BIT::bin => bool => bin)
-                  ((op BIT::bin => bool => bin) (Numeral.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) (Numeral.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 +5509,16 @@
             ((op /::real => real => real) (pi::real)
               ((number_of::bin => real)
                 ((op BIT::bin => bool => bin)
-                  ((op BIT::bin => bool => bin) (Numeral.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) (Numeral.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,7 +5534,8 @@
           ((op ^::real => nat => real) ((tan::real => real) x)
             ((number_of::bin => nat)
               ((op BIT::bin => bool => bin)
-                ((op BIT::bin => bool => bin) (Numeral.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))
@@ -5528,7 +5557,8 @@
             ((op ^::real => nat => real) ((cos::real => real) x)
               ((number_of::bin => nat)
                 ((op BIT::bin => bool => bin)
-                  ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
+                  ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
+                    (True::bool))
                   (False::bool))))))))"
   by (import transc SIN_COS_SQ)
 
@@ -5541,14 +5571,16 @@
             ((op /::real => real => real) (pi::real)
               ((number_of::bin => real)
                 ((op BIT::bin => bool => bin)
-                  ((op BIT::bin => bool => bin) (Numeral.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) (Numeral.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 +5588,8 @@
             ((op ^::real => nat => real) ((sin::real => real) x)
               ((number_of::bin => nat)
                 ((op BIT::bin => bool => bin)
-                  ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
+                  ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
+                    (True::bool))
                   (False::bool))))))))"
   by (import transc COS_SIN_SQ)
 
@@ -5595,7 +5628,8 @@
             ((op ^::real => nat => real) ((sin::real => real) x)
               ((number_of::bin => nat)
                 ((op BIT::bin => bool => bin)
-                  ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
+                  ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
+                    (True::bool))
                   (False::bool))))))))"
   by (import transc COS_SIN_SQRT)
 
@@ -5609,7 +5643,8 @@
             ((op ^::real => nat => real) ((cos::real => real) x)
               ((number_of::bin => nat)
                 ((op BIT::bin => bool => bin)
-                  ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
+                  ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
+                    (True::bool))
                   (False::bool))))))))"
   by (import transc SIN_COS_SQRT)