--- a/src/HOL/Rings.thy Thu Oct 31 11:44:20 2013 +0100
+++ b/src/HOL/Rings.thy Thu Oct 31 11:44:20 2013 +0100
@@ -86,7 +86,20 @@
lemma one_neq_zero [simp]: "1 \<noteq> 0"
by (rule not_sym) (rule zero_neq_one)
-end
+definition of_bool :: "bool \<Rightarrow> 'a"
+where
+ "of_bool p = (if p then 1 else 0)"
+
+lemma of_bool_eq [simp, code]:
+ "of_bool False = 0"
+ "of_bool True = 1"
+ by (simp_all add: of_bool_def)
+
+lemma of_bool_eq_iff:
+ "of_bool p = of_bool q \<longleftrightarrow> p = q"
+ by (simp add: of_bool_def)
+
+end
class semiring_1 = zero_neq_one + semiring_0 + monoid_mult
--- a/src/HOL/Word/Word.thy Thu Oct 31 11:44:20 2013 +0100
+++ b/src/HOL/Word/Word.thy Thu Oct 31 11:44:20 2013 +0100
@@ -506,10 +506,6 @@
definition max_word :: "'a::len word" -- "Largest representable machine integer." where
"max_word = word_of_int (2 ^ len_of TYPE('a) - 1)"
-primrec of_bool :: "bool \<Rightarrow> 'a::len word" where
- "of_bool False = 0"
-| "of_bool True = 1"
-
(* FIXME: only provide one theorem name *)
lemmas of_nth_def = word_set_bits_def