Mercurial Mercurial > repos > isabelle / diff
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/ZF/CardinalArith.thy
changeset 61378 3e04c9ca001a
parent 60770 240563fbf41d
child 61394 6142b282b164 
--- a/src/ZF/CardinalArith.thy	Fri Oct 09 19:51:20 2015 +0200
+++ b/src/ZF/CardinalArith.thy	Fri Oct 09 20:26:03 2015 +0200
@@ -43,10 +43,6 @@
   cadd  (infixl "\<oplus>" 65) and
   cmult  (infixl "\<otimes>" 70)
 
-notation (HTML)
-  cadd  (infixl "\<oplus>" 65) and
-  cmult  (infixl "\<otimes>" 70)
-
 
 lemma Card_Union [simp,intro,TC]:
   assumes A: "\<And>x. x\<in>A \<Longrightarrow> Card(x)" shows "Card(\<Union>(A))"
isabelle