# HG changeset patch
# User haftmann
# Date 1275383931 -7200
# Node ID 32c5251f78cdd5a2c42ae9dac9309d2032f5cdcb
# Parent  7c5311e54ea40e55ef61ad9416c3fe104beba589# Parent  f4d3c929c526d88d96925281019102f664b670b2
merged

diff -r f4d3c929c526 -r 32c5251f78cd src/HOL/Word/WordDefinition.thy
--- a/src/HOL/Word/WordDefinition.thy	Tue Jun 01 10:30:54 2010 +0200
+++ b/src/HOL/Word/WordDefinition.thy	Tue Jun 01 11:18:51 2010 +0200
@@ -19,13 +19,31 @@
 definition word_of_int :: "int \<Rightarrow> 'a\<Colon>len0 word" where
   -- {* representation of words using unsigned or signed bins, 
         only difference in these is the type class *}
-  [code del]: "word_of_int w = Abs_word (bintrunc (len_of TYPE ('a)) w)" 
+  "word_of_int w = Abs_word (bintrunc (len_of TYPE ('a)) w)" 
 
 lemma uint_word_of_int [code]: "uint (word_of_int w \<Colon> 'a\<Colon>len0 word) = w mod 2 ^ len_of TYPE('a)"
   by (auto simp add: word_of_int_def bintrunc_mod2p intro: Abs_word_inverse)
 
 code_datatype word_of_int
 
+notation fcomp (infixl "o>" 60)
+notation scomp (infixl "o\<rightarrow>" 60)
+
+instantiation word :: ("{len0, typerep}") random
+begin
+
+definition
+  "random_word i = Random.range (max i (2 ^ len_of TYPE('a))) o\<rightarrow> (\<lambda>k. Pair (
+     let j = word_of_int (Code_Numeral.int_of k) :: 'a word
+     in (j, \<lambda>_::unit. Code_Evaluation.term_of j)))"
+
+instance ..
+
+end
+
+no_notation fcomp (infixl "o>" 60)
+no_notation scomp (infixl "o\<rightarrow>" 60)
+
 
 subsection {* Type conversions and casting *}