Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned
authorhaftmann
Sat, 13 Apr 2019 08:11:46 +0000
changeset 70144 c925bc0df827
parent 70143 0cc7fe616924
child 70145 f07b8fb99818
tuned
src/HOL/Rings.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Rings.thy	Sat Apr 13 13:30:02 2019 +0200
+++ b/src/HOL/Rings.thy	Sat Apr 13 08:11:46 2019 +0000
@@ -120,7 +120,7 @@
 class semiring_1 = zero_neq_one + semiring_0 + monoid_mult
 begin
 
-lemma (in semiring_1) of_bool_conj:
+lemma of_bool_conj:
   "of_bool (P \<and> Q) = of_bool P * of_bool Q"
   by auto
isabelle