src/HOL/Transitive_Closure.thy
changeset 61378 3e04c9ca001a
parent 61032 b57df8eecad6
child 61424 c3658c18b7bc
--- a/src/HOL/Transitive_Closure.thy	Fri Oct 09 19:51:20 2015 +0200
+++ b/src/HOL/Transitive_Closure.thy	Fri Oct 09 20:26:03 2015 +0200
@@ -59,14 +59,6 @@
   trancl  ("(_\<^sup>+)" [1000] 999) and
   reflcl  ("(_\<^sup>=)" [1000] 999)
 
-notation (HTML output)
-  rtranclp  ("(_\<^sup>*\<^sup>*)" [1000] 1000) and
-  tranclp  ("(_\<^sup>+\<^sup>+)" [1000] 1000) and
-  reflclp  ("(_\<^sup>=\<^sup>=)" [1000] 1000) and
-  rtrancl  ("(_\<^sup>*)" [1000] 999) and
-  trancl  ("(_\<^sup>+)" [1000] 999) and
-  reflcl  ("(_\<^sup>=)" [1000] 999)
-
 
 subsection \<open>Reflexive closure\<close>