src/HOL/Quickcheck.thy
changeset 37751 89e16802b6cc
parent 36176 3fe7e97ccca8
child 38857 97775f3e8722
     1.1 --- a/src/HOL/Quickcheck.thy	Thu Jul 08 17:23:05 2010 +0200
     1.2 +++ b/src/HOL/Quickcheck.thy	Fri Jul 09 08:11:10 2010 +0200
     1.3 @@ -7,8 +7,8 @@
     1.4  uses ("Tools/quickcheck_generators.ML")
     1.5  begin
     1.6  
     1.7 -notation fcomp (infixl "o>" 60)
     1.8 -notation scomp (infixl "o\<rightarrow>" 60)
     1.9 +notation fcomp (infixl "\<circ>>" 60)
    1.10 +notation scomp (infixl "\<circ>\<rightarrow>" 60)
    1.11  
    1.12  
    1.13  subsection {* The @{text random} class *}
    1.14 @@ -23,7 +23,7 @@
    1.15  begin
    1.16  
    1.17  definition
    1.18 -  "random i = Random.range 2 o\<rightarrow>
    1.19 +  "random i = Random.range 2 \<circ>\<rightarrow>
    1.20      (\<lambda>k. Pair (if k = 0 then Code_Evaluation.valtermify False else Code_Evaluation.valtermify True))"
    1.21  
    1.22  instance ..
    1.23 @@ -44,7 +44,7 @@
    1.24  begin
    1.25  
    1.26  definition
    1.27 -  "random _ = Random.select chars o\<rightarrow> (\<lambda>c. Pair (c, \<lambda>u. Code_Evaluation.term_of c))"
    1.28 +  "random _ = Random.select chars \<circ>\<rightarrow> (\<lambda>c. Pair (c, \<lambda>u. Code_Evaluation.term_of c))"
    1.29  
    1.30  instance ..
    1.31  
    1.32 @@ -64,7 +64,7 @@
    1.33  begin
    1.34  
    1.35  definition random_nat :: "code_numeral \<Rightarrow> Random.seed \<Rightarrow> (nat \<times> (unit \<Rightarrow> Code_Evaluation.term)) \<times> Random.seed" where
    1.36 -  "random_nat i = Random.range (i + 1) o\<rightarrow> (\<lambda>k. Pair (
    1.37 +  "random_nat i = Random.range (i + 1) \<circ>\<rightarrow> (\<lambda>k. Pair (
    1.38       let n = Code_Numeral.nat_of k
    1.39       in (n, \<lambda>_. Code_Evaluation.term_of n)))"
    1.40  
    1.41 @@ -76,7 +76,7 @@
    1.42  begin
    1.43  
    1.44  definition
    1.45 -  "random i = Random.range (2 * i + 1) o\<rightarrow> (\<lambda>k. Pair (
    1.46 +  "random i = Random.range (2 * i + 1) \<circ>\<rightarrow> (\<lambda>k. Pair (
    1.47       let j = (if k \<ge> i then Code_Numeral.int_of (k - i) else - Code_Numeral.int_of (i - k))
    1.48       in (j, \<lambda>_. Code_Evaluation.term_of j)))"
    1.49  
    1.50 @@ -110,7 +110,7 @@
    1.51  text {* Towards type copies and datatypes *}
    1.52  
    1.53  definition collapse :: "('a \<Rightarrow> ('a \<Rightarrow> 'b \<times> 'a) \<times> 'a) \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a" where
    1.54 -  "collapse f = (f o\<rightarrow> id)"
    1.55 +  "collapse f = (f \<circ>\<rightarrow> id)"
    1.56  
    1.57  definition beyond :: "code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral" where
    1.58    "beyond k l = (if l > k then l else 0)"
    1.59 @@ -139,8 +139,8 @@
    1.60  
    1.61  code_reserved Quickcheck Quickcheck_Generators
    1.62  
    1.63 -no_notation fcomp (infixl "o>" 60)
    1.64 -no_notation scomp (infixl "o\<rightarrow>" 60)
    1.65 +no_notation fcomp (infixl "\<circ>>" 60)
    1.66 +no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
    1.67  
    1.68  
    1.69  subsection {* The Random-Predicate Monad *}