Mercurial Mercurial > repos > isabelle / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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
isabelle