# HG changeset patch
# User nipkow
# Date 1513876284 -3600
# Node ID d2be0579a2c8723340728d0662b5aecc3042fdca
# Parent  43ed806acb95226cb25dea2981a13b278a0ad0d5
tuned op's

diff -r 43ed806acb95 -r d2be0579a2c8 src/HOL/Library/Numeral_Type.thy
--- a/src/HOL/Library/Numeral_Type.thy	Wed Dec 20 22:07:05 2017 +0100
+++ b/src/HOL/Library/Numeral_Type.thy	Thu Dec 21 18:11:24 2017 +0100
@@ -299,7 +299,7 @@
     (auto simp add: less_eq_bit0_def less_bit0_def less_eq_bit1_def less_bit1_def Rep_bit0_inject Rep_bit1_inject)
 end
 
-lemma (in preorder) tranclp_less: "op <\<^sup>+\<^sup>+ = op <"
+lemma (in preorder) tranclp_less: "op < \<^sup>+\<^sup>+ = op <"
 by(auto simp add: fun_eq_iff intro: less_trans elim: tranclp.induct)
 
 instance bit0 and bit1 :: (finite) wellorder