src/HOL/Rings.thy
changeset 70144 c925bc0df827
parent 70094 a93e6472ac9c
child 70145 f07b8fb99818
equal deleted inserted replaced
70143:0cc7fe616924 70144:c925bc0df827
   118 end
   118 end
   119 
   119 
   120 class semiring_1 = zero_neq_one + semiring_0 + monoid_mult
   120 class semiring_1 = zero_neq_one + semiring_0 + monoid_mult
   121 begin
   121 begin
   122 
   122 
   123 lemma (in semiring_1) of_bool_conj:
   123 lemma of_bool_conj:
   124   "of_bool (P \<and> Q) = of_bool P * of_bool Q"
   124   "of_bool (P \<and> Q) = of_bool P * of_bool Q"
   125   by auto
   125   by auto
   126 
   126 
   127 end
   127 end
   128 
   128