--- a/src/HOL/Import/HOL/HOL4Prob.thy Wed Jun 30 14:04:58 2004 +0200
+++ b/src/HOL/Import/HOL/HOL4Prob.thy Thu Jul 01 12:29:53 2004 +0200
@@ -27,7 +27,7 @@
((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)))
q)
@@ -40,14 +40,14 @@
((op div::nat => nat => nat) 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)))))
((op =::nat => nat => bool) r
((op mod::nat => nat => nat) 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)))))))))"
by (import prob_extra DIV_TWO_UNIQUE)
@@ -76,13 +76,13 @@
((op div::nat => nat => nat) m
((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))))
((op div::nat => nat => nat) 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)))))
((op <::nat => nat => bool) m n)))"
@@ -98,13 +98,13 @@
((op div::nat => nat => nat) m
((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))))
((op div::nat => nat => nat) 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)))))
((op <::nat => nat => bool) m n))))"
@@ -204,7 +204,7 @@
((op /::real => real => real) (1::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))))
n)
@@ -212,7 +212,7 @@
((op /::real => real => real) (1::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))))
m))))"
@@ -2528,7 +2528,7 @@
((op /::real => real => real) (1::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))))
((prob::((nat => bool) => bool) => real) p)))))"
@@ -3156,7 +3156,7 @@
((op /::real => real => real) (1::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))))
((size::bool list => nat) x))
@@ -3382,7 +3382,7 @@
(P ((op div::nat => nat => nat) ((Suc::nat => nat) v)
((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)))))
(P ((Suc::nat => nat) v)))))
@@ -3436,7 +3436,7 @@
(P ((op div::nat => nat => nat) ((Suc::nat => nat) v2)
((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))))
s)
@@ -3716,13 +3716,13 @@
((op ^::nat => nat => nat)
((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)))
((unif_bound::nat => nat) n))
((op *::nat => nat => nat)
((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)))
n)))"
by (import prob_uniform UNIF_BOUND_UPPER)
@@ -3771,7 +3771,7 @@
((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)))
((unif_bound::nat => nat) n)))
@@ -3788,7 +3788,7 @@
((op /::real => real => real) (1::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))))
((unif_bound::nat => nat) n))))))"
@@ -3907,7 +3907,7 @@
((op /::real => real => real) (1::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))))
t))))))"
@@ -3938,7 +3938,7 @@
((op /::real => real => real) (1::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))))
t)))))"
@@ -3969,7 +3969,7 @@
((op /::real => real => real) (1::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))))
t)))))"