--- a/src/HOL/Archimedean_Field.thy Fri Oct 09 19:51:20 2015 +0200
+++ b/src/HOL/Archimedean_Field.thy Fri Oct 09 20:26:03 2015 +0200
@@ -144,9 +144,6 @@
notation (xsymbols)
floor ("\<lfloor>_\<rfloor>")
-notation (HTML output)
- floor ("\<lfloor>_\<rfloor>")
-
lemma floor_unique: "\<lbrakk>of_int z \<le> x; x < of_int z + 1\<rbrakk> \<Longrightarrow> floor x = z"
using floor_correct [of x] floor_exists1 [of x] by auto
@@ -383,9 +380,6 @@
notation (xsymbols)
ceiling ("\<lceil>_\<rceil>")
-notation (HTML output)
- ceiling ("\<lceil>_\<rceil>")
-
lemma ceiling_correct: "of_int (ceiling x) - 1 < x \<and> x \<le> of_int (ceiling x)"
unfolding ceiling_def using floor_correct [of "- x"] by simp