src/HOL/Word/Word.thy
changeset 54225 8a49a5a30284
parent 54224 9fda41a04c32
child 54489 03ff4d1e6784
     1.1 --- a/src/HOL/Word/Word.thy	Thu Oct 31 11:44:20 2013 +0100
     1.2 +++ b/src/HOL/Word/Word.thy	Thu Oct 31 11:44:20 2013 +0100
     1.3 @@ -506,10 +506,6 @@
     1.4  definition max_word :: "'a::len word" -- "Largest representable machine integer." where
     1.5    "max_word = word_of_int (2 ^ len_of TYPE('a) - 1)"
     1.6  
     1.7 -primrec of_bool :: "bool \<Rightarrow> 'a::len word" where
     1.8 -  "of_bool False = 0"
     1.9 -| "of_bool True = 1"
    1.10 -
    1.11  (* FIXME: only provide one theorem name *)
    1.12  lemmas of_nth_def = word_set_bits_def
    1.13