nicer xsymbol syntax for fcomp and scomp
authorhaftmann
Fri Jul 09 08:11:10 2010 +0200 (2010-07-09)
changeset 3775189e16802b6cc
parent 37750 82e0fe8b07eb
child 37752 d0a384c84d69
nicer xsymbol syntax for fcomp and scomp
src/HOL/Fun.thy
src/HOL/Library/Fset.thy
src/HOL/Library/Multiset.thy
src/HOL/Library/State_Monad.thy
src/HOL/Product_Type.thy
src/HOL/Quickcheck.thy
src/HOL/Random.thy
src/HOL/Rat.thy
src/HOL/RealDef.thy
src/HOL/Word/Word.thy
     1.1 --- a/src/HOL/Fun.thy	Thu Jul 08 17:23:05 2010 +0200
     1.2 +++ b/src/HOL/Fun.thy	Fri Jul 09 08:11:10 2010 +0200
     1.3 @@ -95,26 +95,26 @@
     1.4  subsection {* The Forward Composition Operator @{text fcomp} *}
     1.5  
     1.6  definition
     1.7 -  fcomp :: "('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> 'a \<Rightarrow> 'c" (infixl "o>" 60)
     1.8 +  fcomp :: "('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> 'a \<Rightarrow> 'c" (infixl "\<circ>>" 60)
     1.9  where
    1.10 -  "f o> g = (\<lambda>x. g (f x))"
    1.11 +  "f \<circ>> g = (\<lambda>x. g (f x))"
    1.12  
    1.13 -lemma fcomp_apply:  "(f o> g) x = g (f x)"
    1.14 +lemma fcomp_apply [simp]:  "(f \<circ>> g) x = g (f x)"
    1.15    by (simp add: fcomp_def)
    1.16  
    1.17 -lemma fcomp_assoc: "(f o> g) o> h = f o> (g o> h)"
    1.18 +lemma fcomp_assoc: "(f \<circ>> g) \<circ>> h = f \<circ>> (g \<circ>> h)"
    1.19    by (simp add: fcomp_def)
    1.20  
    1.21 -lemma id_fcomp [simp]: "id o> g = g"
    1.22 +lemma id_fcomp [simp]: "id \<circ>> g = g"
    1.23    by (simp add: fcomp_def)
    1.24  
    1.25 -lemma fcomp_id [simp]: "f o> id = f"
    1.26 +lemma fcomp_id [simp]: "f \<circ>> id = f"
    1.27    by (simp add: fcomp_def)
    1.28  
    1.29  code_const fcomp
    1.30    (Eval infixl 1 "#>")
    1.31  
    1.32 -no_notation fcomp (infixl "o>" 60)
    1.33 +no_notation fcomp (infixl "\<circ>>" 60)
    1.34  
    1.35  
    1.36  subsection {* Injectivity and Surjectivity *}
     2.1 --- a/src/HOL/Library/Fset.thy	Thu Jul 08 17:23:05 2010 +0200
     2.2 +++ b/src/HOL/Library/Fset.thy	Fri Jul 09 08:11:10 2010 +0200
     2.3 @@ -69,21 +69,21 @@
     2.4      \<Rightarrow> 'a fset \<times> (unit \<Rightarrow> Code_Evaluation.term)" where
     2.5    [code_unfold]: "setify xs = Code_Evaluation.valtermify Set {\<cdot>} xs"
     2.6  
     2.7 -notation fcomp (infixl "o>" 60)
     2.8 -notation scomp (infixl "o\<rightarrow>" 60)
     2.9 +notation fcomp (infixl "\<circ>>" 60)
    2.10 +notation scomp (infixl "\<circ>\<rightarrow>" 60)
    2.11  
    2.12  instantiation fset :: (random) random
    2.13  begin
    2.14  
    2.15  definition
    2.16 -  "Quickcheck.random i = Quickcheck.random i o\<rightarrow> (\<lambda>xs. Pair (setify xs))"
    2.17 +  "Quickcheck.random i = Quickcheck.random i \<circ>\<rightarrow> (\<lambda>xs. Pair (setify xs))"
    2.18  
    2.19  instance ..
    2.20  
    2.21  end
    2.22  
    2.23 -no_notation fcomp (infixl "o>" 60)
    2.24 -no_notation scomp (infixl "o\<rightarrow>" 60)
    2.25 +no_notation fcomp (infixl "\<circ>>" 60)
    2.26 +no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
    2.27  
    2.28  
    2.29  subsection {* Lattice instantiation *}
     3.1 --- a/src/HOL/Library/Multiset.thy	Thu Jul 08 17:23:05 2010 +0200
     3.2 +++ b/src/HOL/Library/Multiset.thy	Fri Jul 09 08:11:10 2010 +0200
     3.3 @@ -954,21 +954,21 @@
     3.4      \<Rightarrow> 'a multiset \<times> (unit \<Rightarrow> Code_Evaluation.term)" where
     3.5    [code_unfold]: "bagify xs = Code_Evaluation.valtermify Bag {\<cdot>} xs"
     3.6  
     3.7 -notation fcomp (infixl "o>" 60)
     3.8 -notation scomp (infixl "o\<rightarrow>" 60)
     3.9 +notation fcomp (infixl "\<circ>>" 60)
    3.10 +notation scomp (infixl "\<circ>\<rightarrow>" 60)
    3.11  
    3.12  instantiation multiset :: (random) random
    3.13  begin
    3.14  
    3.15  definition
    3.16 -  "Quickcheck.random i = Quickcheck.random i o\<rightarrow> (\<lambda>xs. Pair (bagify xs))"
    3.17 +  "Quickcheck.random i = Quickcheck.random i \<circ>\<rightarrow> (\<lambda>xs. Pair (bagify xs))"
    3.18  
    3.19  instance ..
    3.20  
    3.21  end
    3.22  
    3.23 -no_notation fcomp (infixl "o>" 60)
    3.24 -no_notation scomp (infixl "o\<rightarrow>" 60)
    3.25 +no_notation fcomp (infixl "\<circ>>" 60)
    3.26 +no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
    3.27  
    3.28  hide_const (open) bagify
    3.29  
     4.1 --- a/src/HOL/Library/State_Monad.thy	Thu Jul 08 17:23:05 2010 +0200
     4.2 +++ b/src/HOL/Library/State_Monad.thy	Fri Jul 09 08:11:10 2010 +0200
     4.3 @@ -55,23 +55,23 @@
     4.4    we use a set of monad combinators:
     4.5  *}
     4.6  
     4.7 -notation fcomp (infixl "o>" 60)
     4.8 -notation (xsymbols) fcomp (infixl "o>" 60)
     4.9 +notation fcomp (infixl "\<circ>>" 60)
    4.10 +notation (xsymbols) fcomp (infixl "\<circ>>" 60)
    4.11  notation scomp (infixl "o->" 60)
    4.12 -notation (xsymbols) scomp (infixl "o\<rightarrow>" 60)
    4.13 +notation (xsymbols) scomp (infixl "\<circ>\<rightarrow>" 60)
    4.14  
    4.15  abbreviation (input)
    4.16    "return \<equiv> Pair"
    4.17  
    4.18  text {*
    4.19    Given two transformations @{term f} and @{term g}, they
    4.20 -  may be directly composed using the @{term "op o>"} combinator,
    4.21 -  forming a forward composition: @{prop "(f o> g) s = f (g s)"}.
    4.22 +  may be directly composed using the @{term "op \<circ>>"} combinator,
    4.23 +  forming a forward composition: @{prop "(f \<circ>> g) s = f (g s)"}.
    4.24  
    4.25    After any yielding transformation, we bind the side result
    4.26    immediately using a lambda abstraction.  This 
    4.27 -  is the purpose of the @{term "op o\<rightarrow>"} combinator:
    4.28 -  @{prop "(f o\<rightarrow> (\<lambda>x. g)) s = (let (x, s') = f s in g s')"}.
    4.29 +  is the purpose of the @{term "op \<circ>\<rightarrow>"} combinator:
    4.30 +  @{prop "(f \<circ>\<rightarrow> (\<lambda>x. g)) s = (let (x, s') = f s in g s')"}.
    4.31  
    4.32    For queries, the existing @{term "Let"} is appropriate.
    4.33  
    4.34 @@ -141,8 +141,8 @@
    4.35  
    4.36  translations
    4.37    "_do f" => "f"
    4.38 -  "_scomp x f g" => "f o\<rightarrow> (\<lambda>x. g)"
    4.39 -  "_fcomp f g" => "f o> g"
    4.40 +  "_scomp x f g" => "f \<circ>\<rightarrow> (\<lambda>x. g)"
    4.41 +  "_fcomp f g" => "f \<circ>> g"
    4.42    "_let x t f" => "CONST Let t (\<lambda>x. f)"
    4.43    "_done f" => "f"
    4.44  
     5.1 --- a/src/HOL/Product_Type.thy	Thu Jul 08 17:23:05 2010 +0200
     5.2 +++ b/src/HOL/Product_Type.thy	Fri Jul 09 08:11:10 2010 +0200
     5.3 @@ -791,37 +791,37 @@
     5.4    The composition-uncurry combinator.
     5.5  *}
     5.6  
     5.7 -notation fcomp (infixl "o>" 60)
     5.8 +notation fcomp (infixl "\<circ>>" 60)
     5.9  
    5.10 -definition scomp :: "('a \<Rightarrow> 'b \<times> 'c) \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> 'd) \<Rightarrow> 'a \<Rightarrow> 'd" (infixl "o\<rightarrow>" 60) where
    5.11 -  "f o\<rightarrow> g = (\<lambda>x. split g (f x))"
    5.12 +definition scomp :: "('a \<Rightarrow> 'b \<times> 'c) \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> 'd) \<Rightarrow> 'a \<Rightarrow> 'd" (infixl "\<circ>\<rightarrow>" 60) where
    5.13 +  "f \<circ>\<rightarrow> g = (\<lambda>x. prod_case g (f x))"
    5.14  
    5.15  lemma scomp_unfold: "scomp = (\<lambda>f g x. g (fst (f x)) (snd (f x)))"
    5.16 -  by (simp add: expand_fun_eq scomp_def split_def)
    5.17 +  by (simp add: expand_fun_eq scomp_def prod_case_unfold)
    5.18  
    5.19 -lemma scomp_apply:  "(f o\<rightarrow> g) x = split g (f x)"
    5.20 -  by (simp add: scomp_unfold split_def)
    5.21 +lemma scomp_apply [simp]: "(f \<circ>\<rightarrow> g) x = prod_case g (f x)"
    5.22 +  by (simp add: scomp_unfold prod_case_unfold)
    5.23  
    5.24 -lemma Pair_scomp: "Pair x o\<rightarrow> f = f x"
    5.25 +lemma Pair_scomp: "Pair x \<circ>\<rightarrow> f = f x"
    5.26    by (simp add: expand_fun_eq scomp_apply)
    5.27  
    5.28 -lemma scomp_Pair: "x o\<rightarrow> Pair = x"
    5.29 +lemma scomp_Pair: "x \<circ>\<rightarrow> Pair = x"
    5.30    by (simp add: expand_fun_eq scomp_apply)
    5.31  
    5.32 -lemma scomp_scomp: "(f o\<rightarrow> g) o\<rightarrow> h = f o\<rightarrow> (\<lambda>x. g x o\<rightarrow> h)"
    5.33 +lemma scomp_scomp: "(f \<circ>\<rightarrow> g) \<circ>\<rightarrow> h = f \<circ>\<rightarrow> (\<lambda>x. g x \<circ>\<rightarrow> h)"
    5.34    by (simp add: expand_fun_eq scomp_unfold)
    5.35  
    5.36 -lemma scomp_fcomp: "(f o\<rightarrow> g) o> h = f o\<rightarrow> (\<lambda>x. g x o> h)"
    5.37 +lemma scomp_fcomp: "(f \<circ>\<rightarrow> g) \<circ>> h = f \<circ>\<rightarrow> (\<lambda>x. g x \<circ>> h)"
    5.38    by (simp add: expand_fun_eq scomp_unfold fcomp_def)
    5.39  
    5.40 -lemma fcomp_scomp: "(f o> g) o\<rightarrow> h = f o> (g o\<rightarrow> h)"
    5.41 +lemma fcomp_scomp: "(f \<circ>> g) \<circ>\<rightarrow> h = f \<circ>> (g \<circ>\<rightarrow> h)"
    5.42    by (simp add: expand_fun_eq scomp_unfold fcomp_apply)
    5.43  
    5.44  code_const scomp
    5.45    (Eval infixl 3 "#->")
    5.46  
    5.47 -no_notation fcomp (infixl "o>" 60)
    5.48 -no_notation scomp (infixl "o\<rightarrow>" 60)
    5.49 +no_notation fcomp (infixl "\<circ>>" 60)
    5.50 +no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
    5.51  
    5.52  text {*
    5.53    @{term prod_fun} --- action of the product functor upon
     6.1 --- a/src/HOL/Quickcheck.thy	Thu Jul 08 17:23:05 2010 +0200
     6.2 +++ b/src/HOL/Quickcheck.thy	Fri Jul 09 08:11:10 2010 +0200
     6.3 @@ -7,8 +7,8 @@
     6.4  uses ("Tools/quickcheck_generators.ML")
     6.5  begin
     6.6  
     6.7 -notation fcomp (infixl "o>" 60)
     6.8 -notation scomp (infixl "o\<rightarrow>" 60)
     6.9 +notation fcomp (infixl "\<circ>>" 60)
    6.10 +notation scomp (infixl "\<circ>\<rightarrow>" 60)
    6.11  
    6.12  
    6.13  subsection {* The @{text random} class *}
    6.14 @@ -23,7 +23,7 @@
    6.15  begin
    6.16  
    6.17  definition
    6.18 -  "random i = Random.range 2 o\<rightarrow>
    6.19 +  "random i = Random.range 2 \<circ>\<rightarrow>
    6.20      (\<lambda>k. Pair (if k = 0 then Code_Evaluation.valtermify False else Code_Evaluation.valtermify True))"
    6.21  
    6.22  instance ..
    6.23 @@ -44,7 +44,7 @@
    6.24  begin
    6.25  
    6.26  definition
    6.27 -  "random _ = Random.select chars o\<rightarrow> (\<lambda>c. Pair (c, \<lambda>u. Code_Evaluation.term_of c))"
    6.28 +  "random _ = Random.select chars \<circ>\<rightarrow> (\<lambda>c. Pair (c, \<lambda>u. Code_Evaluation.term_of c))"
    6.29  
    6.30  instance ..
    6.31  
    6.32 @@ -64,7 +64,7 @@
    6.33  begin
    6.34  
    6.35  definition random_nat :: "code_numeral \<Rightarrow> Random.seed \<Rightarrow> (nat \<times> (unit \<Rightarrow> Code_Evaluation.term)) \<times> Random.seed" where
    6.36 -  "random_nat i = Random.range (i + 1) o\<rightarrow> (\<lambda>k. Pair (
    6.37 +  "random_nat i = Random.range (i + 1) \<circ>\<rightarrow> (\<lambda>k. Pair (
    6.38       let n = Code_Numeral.nat_of k
    6.39       in (n, \<lambda>_. Code_Evaluation.term_of n)))"
    6.40  
    6.41 @@ -76,7 +76,7 @@
    6.42  begin
    6.43  
    6.44  definition
    6.45 -  "random i = Random.range (2 * i + 1) o\<rightarrow> (\<lambda>k. Pair (
    6.46 +  "random i = Random.range (2 * i + 1) \<circ>\<rightarrow> (\<lambda>k. Pair (
    6.47       let j = (if k \<ge> i then Code_Numeral.int_of (k - i) else - Code_Numeral.int_of (i - k))
    6.48       in (j, \<lambda>_. Code_Evaluation.term_of j)))"
    6.49  
    6.50 @@ -110,7 +110,7 @@
    6.51  text {* Towards type copies and datatypes *}
    6.52  
    6.53  definition collapse :: "('a \<Rightarrow> ('a \<Rightarrow> 'b \<times> 'a) \<times> 'a) \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a" where
    6.54 -  "collapse f = (f o\<rightarrow> id)"
    6.55 +  "collapse f = (f \<circ>\<rightarrow> id)"
    6.56  
    6.57  definition beyond :: "code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral" where
    6.58    "beyond k l = (if l > k then l else 0)"
    6.59 @@ -139,8 +139,8 @@
    6.60  
    6.61  code_reserved Quickcheck Quickcheck_Generators
    6.62  
    6.63 -no_notation fcomp (infixl "o>" 60)
    6.64 -no_notation scomp (infixl "o\<rightarrow>" 60)
    6.65 +no_notation fcomp (infixl "\<circ>>" 60)
    6.66 +no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
    6.67  
    6.68  
    6.69  subsection {* The Random-Predicate Monad *} 
     7.1 --- a/src/HOL/Random.thy	Thu Jul 08 17:23:05 2010 +0200
     7.2 +++ b/src/HOL/Random.thy	Fri Jul 09 08:11:10 2010 +0200
     7.3 @@ -7,8 +7,8 @@
     7.4  imports Code_Numeral List
     7.5  begin
     7.6  
     7.7 -notation fcomp (infixl "o>" 60)
     7.8 -notation scomp (infixl "o\<rightarrow>" 60)
     7.9 +notation fcomp (infixl "\<circ>>" 60)
    7.10 +notation scomp (infixl "\<circ>\<rightarrow>" 60)
    7.11  
    7.12  
    7.13  subsection {* Auxiliary functions *}
    7.14 @@ -48,12 +48,12 @@
    7.15  subsection {* Base selectors *}
    7.16  
    7.17  fun iterate :: "code_numeral \<Rightarrow> ('b \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a" where
    7.18 -  "iterate k f x = (if k = 0 then Pair x else f x o\<rightarrow> iterate (k - 1) f)"
    7.19 +  "iterate k f x = (if k = 0 then Pair x else f x \<circ>\<rightarrow> iterate (k - 1) f)"
    7.20  
    7.21  definition range :: "code_numeral \<Rightarrow> seed \<Rightarrow> code_numeral \<times> seed" where
    7.22    "range k = iterate (log 2147483561 k)
    7.23 -      (\<lambda>l. next o\<rightarrow> (\<lambda>v. Pair (v + l * 2147483561))) 1
    7.24 -    o\<rightarrow> (\<lambda>v. Pair (v mod k))"
    7.25 +      (\<lambda>l. next \<circ>\<rightarrow> (\<lambda>v. Pair (v + l * 2147483561))) 1
    7.26 +    \<circ>\<rightarrow> (\<lambda>v. Pair (v mod k))"
    7.27  
    7.28  lemma range:
    7.29    "k > 0 \<Longrightarrow> fst (range k s) < k"
    7.30 @@ -61,7 +61,7 @@
    7.31  
    7.32  definition select :: "'a list \<Rightarrow> seed \<Rightarrow> 'a \<times> seed" where
    7.33    "select xs = range (Code_Numeral.of_nat (length xs))
    7.34 -    o\<rightarrow> (\<lambda>k. Pair (nth xs (Code_Numeral.nat_of k)))"
    7.35 +    \<circ>\<rightarrow> (\<lambda>k. Pair (nth xs (Code_Numeral.nat_of k)))"
    7.36       
    7.37  lemma select:
    7.38    assumes "xs \<noteq> []"
    7.39 @@ -97,7 +97,7 @@
    7.40  
    7.41  definition select_weight :: "(code_numeral \<times> 'a) list \<Rightarrow> seed \<Rightarrow> 'a \<times> seed" where
    7.42    "select_weight xs = range (listsum (map fst xs))
    7.43 -   o\<rightarrow> (\<lambda>k. Pair (pick xs k))"
    7.44 +   \<circ>\<rightarrow> (\<lambda>k. Pair (pick xs k))"
    7.45  
    7.46  lemma select_weight_member:
    7.47    assumes "0 < listsum (map fst xs)"
    7.48 @@ -184,8 +184,8 @@
    7.49    iterate range select pick select_weight
    7.50  hide_fact (open) range_def
    7.51  
    7.52 -no_notation fcomp (infixl "o>" 60)
    7.53 -no_notation scomp (infixl "o\<rightarrow>" 60)
    7.54 +no_notation fcomp (infixl "\<circ>>" 60)
    7.55 +no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
    7.56  
    7.57  end
    7.58  
     8.1 --- a/src/HOL/Rat.thy	Thu Jul 08 17:23:05 2010 +0200
     8.2 +++ b/src/HOL/Rat.thy	Fri Jul 09 08:11:10 2010 +0200
     8.3 @@ -1114,14 +1114,14 @@
     8.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
     8.5    [code_unfold]: "valterm_fract k l = Code_Evaluation.valtermify Fract {\<cdot>} k {\<cdot>} l"
     8.6  
     8.7 -notation fcomp (infixl "o>" 60)
     8.8 -notation scomp (infixl "o\<rightarrow>" 60)
     8.9 +notation fcomp (infixl "\<circ>>" 60)
    8.10 +notation scomp (infixl "\<circ>\<rightarrow>" 60)
    8.11  
    8.12  instantiation rat :: random
    8.13  begin
    8.14  
    8.15  definition
    8.16 -  "Quickcheck.random i = Quickcheck.random i o\<rightarrow> (\<lambda>num. Random.range i o\<rightarrow> (\<lambda>denom. Pair (
    8.17 +  "Quickcheck.random i = Quickcheck.random i \<circ>\<rightarrow> (\<lambda>num. Random.range i \<circ>\<rightarrow> (\<lambda>denom. Pair (
    8.18       let j = Code_Numeral.int_of (denom + 1)
    8.19       in valterm_fract num (j, \<lambda>u. Code_Evaluation.term_of j))))"
    8.20  
    8.21 @@ -1129,8 +1129,8 @@
    8.22  
    8.23  end
    8.24  
    8.25 -no_notation fcomp (infixl "o>" 60)
    8.26 -no_notation scomp (infixl "o\<rightarrow>" 60)
    8.27 +no_notation fcomp (infixl "\<circ>>" 60)
    8.28 +no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
    8.29  
    8.30  text {* Setup for SML code generator *}
    8.31  
     9.1 --- a/src/HOL/RealDef.thy	Thu Jul 08 17:23:05 2010 +0200
     9.2 +++ b/src/HOL/RealDef.thy	Fri Jul 09 08:11:10 2010 +0200
     9.3 @@ -1743,21 +1743,21 @@
     9.4    valterm_ratreal :: "rat \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow> real \<times> (unit \<Rightarrow> Code_Evaluation.term)" where
     9.5    [code_unfold]: "valterm_ratreal k = Code_Evaluation.valtermify Ratreal {\<cdot>} k"
     9.6  
     9.7 -notation fcomp (infixl "o>" 60)
     9.8 -notation scomp (infixl "o\<rightarrow>" 60)
     9.9 +notation fcomp (infixl "\<circ>>" 60)
    9.10 +notation scomp (infixl "\<circ>\<rightarrow>" 60)
    9.11  
    9.12  instantiation real :: random
    9.13  begin
    9.14  
    9.15  definition
    9.16 -  "Quickcheck.random i = Quickcheck.random i o\<rightarrow> (\<lambda>r. Pair (valterm_ratreal r))"
    9.17 +  "Quickcheck.random i = Quickcheck.random i \<circ>\<rightarrow> (\<lambda>r. Pair (valterm_ratreal r))"
    9.18  
    9.19  instance ..
    9.20  
    9.21  end
    9.22  
    9.23 -no_notation fcomp (infixl "o>" 60)
    9.24 -no_notation scomp (infixl "o\<rightarrow>" 60)
    9.25 +no_notation fcomp (infixl "\<circ>>" 60)
    9.26 +no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
    9.27  
    9.28  text {* Setup for SML code generator *}
    9.29  
    10.1 --- a/src/HOL/Word/Word.thy	Thu Jul 08 17:23:05 2010 +0200
    10.2 +++ b/src/HOL/Word/Word.thy	Fri Jul 09 08:11:10 2010 +0200
    10.3 @@ -26,14 +26,14 @@
    10.4  
    10.5  code_datatype word_of_int
    10.6  
    10.7 -notation fcomp (infixl "o>" 60)
    10.8 -notation scomp (infixl "o\<rightarrow>" 60)
    10.9 +notation fcomp (infixl "\<circ>>" 60)
   10.10 +notation scomp (infixl "\<circ>\<rightarrow>" 60)
   10.11  
   10.12  instantiation word :: ("{len0, typerep}") random
   10.13  begin
   10.14  
   10.15  definition
   10.16 -  "random_word i = Random.range (max i (2 ^ len_of TYPE('a))) o\<rightarrow> (\<lambda>k. Pair (
   10.17 +  "random_word i = Random.range (max i (2 ^ len_of TYPE('a))) \<circ>\<rightarrow> (\<lambda>k. Pair (
   10.18       let j = word_of_int (Code_Numeral.int_of k) :: 'a word
   10.19       in (j, \<lambda>_::unit. Code_Evaluation.term_of j)))"
   10.20  
   10.21 @@ -41,8 +41,8 @@
   10.22  
   10.23  end
   10.24  
   10.25 -no_notation fcomp (infixl "o>" 60)
   10.26 -no_notation scomp (infixl "o\<rightarrow>" 60)
   10.27 +no_notation fcomp (infixl "\<circ>>" 60)
   10.28 +no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
   10.29  
   10.30  
   10.31  subsection {* Type conversions and casting *}