# HG changeset patch
# User wenzelm
# Date 1090420538 -7200
# Node ID b65fc0787fbef7efa624a030d0d2b7024d50bc7b
# Parent  541d2a35fc30e9fcaa4b98bfc1086fdc11021518
updated;

diff -r 541d2a35fc30 -r b65fc0787fbe src/HOL/Import/HOL/HOL4Prob.thy
--- a/src/HOL/Import/HOL/HOL4Prob.thy	Wed Jul 21 08:35:29 2004 +0200
+++ b/src/HOL/Import/HOL/HOL4Prob.thy	Wed Jul 21 16:35:38 2004 +0200
@@ -3156,8 +3156,8 @@
                           ((op /::real => real => real) (1::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))))
                           ((size::bool list => nat) x))
                         ((prob::((nat => bool) => bool) => real) q))))))))"
@@ -3436,8 +3436,8 @@
                     (P ((op div::nat => nat => nat) ((Suc::nat => nat) v2)
                          ((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))))
                       s)
                     (P ((Suc::nat => nat) v2) s)))))
@@ -3907,8 +3907,8 @@
                          ((op /::real => real => real) (1::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))))
                          t))))))"
   by (import prob_uniform PROB_UNIFORM_PAIR_SUC)
diff -r 541d2a35fc30 -r b65fc0787fbe src/HOL/Import/HOL/HOL4Real.thy
--- 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)
 
diff -r 541d2a35fc30 -r b65fc0787fbe src/HOL/Import/HOL/HOL4Vec.thy
--- a/src/HOL/Import/HOL/HOL4Vec.thy	Wed Jul 21 08:35:29 2004 +0200
+++ b/src/HOL/Import/HOL/HOL4Vec.thy	Wed Jul 21 16:35:38 2004 +0200
@@ -1298,8 +1298,8 @@
                          ((op ^::nat => nat => nat)
                            ((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)))
                            k)))))))"
   by (import bword_arith ACARRY_EQ_ADD_DIV)