src/HOL/Rat.thy
changeset 37751 89e16802b6cc
parent 37397 18000f9d783e
child 38242 f26d590dce0f
     1.1 --- a/src/HOL/Rat.thy	Thu Jul 08 17:23:05 2010 +0200
     1.2 +++ b/src/HOL/Rat.thy	Fri Jul 09 08:11:10 2010 +0200
     1.3 @@ -1114,14 +1114,14 @@
     1.4    valterm_fract :: "int \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow> int \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow> rat \<times> (unit \<Rightarrow> Code_Evaluation.term)" where
     1.5    [code_unfold]: "valterm_fract k l = Code_Evaluation.valtermify Fract {\<cdot>} k {\<cdot>} l"
     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  instantiation rat :: random
    1.13  begin
    1.14  
    1.15  definition
    1.16 -  "Quickcheck.random i = Quickcheck.random i o\<rightarrow> (\<lambda>num. Random.range i o\<rightarrow> (\<lambda>denom. Pair (
    1.17 +  "Quickcheck.random i = Quickcheck.random i \<circ>\<rightarrow> (\<lambda>num. Random.range i \<circ>\<rightarrow> (\<lambda>denom. Pair (
    1.18       let j = Code_Numeral.int_of (denom + 1)
    1.19       in valterm_fract num (j, \<lambda>u. Code_Evaluation.term_of j))))"
    1.20  
    1.21 @@ -1129,8 +1129,8 @@
    1.22  
    1.23  end
    1.24  
    1.25 -no_notation fcomp (infixl "o>" 60)
    1.26 -no_notation scomp (infixl "o\<rightarrow>" 60)
    1.27 +no_notation fcomp (infixl "\<circ>>" 60)
    1.28 +no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
    1.29  
    1.30  text {* Setup for SML code generator *}
    1.31