# HG changeset patch
# User wenzelm
# Date 1444509885 -7200
# Node ID 808222c1cf662ef9efab04a95c27d1037e661987
# Parent  6794de67556813ff8e4fac158e31a7e55215c40e
tuned syntax -- less symbols;

diff -r 6794de675568 -r 808222c1cf66 src/ZF/OrderType.thy
--- a/src/ZF/OrderType.thy	Sat Oct 10 22:40:56 2015 +0200
+++ b/src/ZF/OrderType.thy	Sat Oct 10 22:44:45 2015 +0200
@@ -49,10 +49,6 @@
     "i -- j == ordertype(i-j, Memrel(i))"
 
 
-notation (xsymbols)
-  omult  (infixl "\<times>\<times>" 70)
-
-
 subsection\<open>Proofs needing the combination of Ordinal.thy and Order.thy\<close>
 
 lemma le_well_ord_Memrel: "j \<le> i ==> well_ord(j, Memrel(i))"
@@ -973,7 +969,7 @@
       by simp
   next
     case (succ i)
-    have "j \<times>\<times> i ++ 0 < j \<times>\<times> i ++ j"
+    have "j ** i ++ 0 < j ** i ++ j"
       by (rule oadd_lt_mono2 [OF j])
     with succ.hyps show ?case
       by (simp add: oj j omult_succ ) (rule lt_trans1)