# HG changeset patch
# User blanchet
# Date 1390238696 -3600
# Node ID 6d0af3c108648c7e2810f1fcefd7804dde69436c
# Parent  8dd21c4b0501e1c185f52dc037003d653962a5d3
compile

diff -r 8dd21c4b0501 -r 6d0af3c10864 src/HOL/Cardinals/Cardinal_Arithmetic.thy
--- a/src/HOL/Cardinals/Cardinal_Arithmetic.thy	Mon Jan 20 18:24:56 2014 +0100
+++ b/src/HOL/Cardinals/Cardinal_Arithmetic.thy	Mon Jan 20 18:24:56 2014 +0100
@@ -11,6 +11,15 @@
 imports BNF_Cardinal_Arithmetic Cardinal_Order_Relation
 begin
 
+notation ordLeq2 (infix "<=o" 50) and
+  ordLeq3 (infix "\<le>o" 50) and
+  ordLess2 (infix "<o" 50) and
+  ordIso2 (infix "=o" 50) and
+  csum (infixr "+c" 65) and
+  cprod (infixr "*c" 80) and
+  cexp (infixr "^c" 90)
+
+
 subsection {* Binary sum *}
 
 lemma csum_Cnotzero2:
diff -r 8dd21c4b0501 -r 6d0af3c10864 src/HOL/Cardinals/Constructions_on_Wellorders.thy
--- a/src/HOL/Cardinals/Constructions_on_Wellorders.thy	Mon Jan 20 18:24:56 2014 +0100
+++ b/src/HOL/Cardinals/Constructions_on_Wellorders.thy	Mon Jan 20 18:24:56 2014 +0100
@@ -11,6 +11,11 @@
 imports BNF_Constructions_on_Wellorders Wellorder_Embedding Order_Union
 begin
 
+notation ordLeq2 (infix "<=o" 50) and
+  ordLeq3 (infix "\<le>o" 50) and
+  ordLess2 (infix "<o" 50) and
+  ordIso2 (infix "=o" 50)
+
 declare
   ordLeq_Well_order_simp[simp]
   not_ordLeq_iff_ordLess[simp]
diff -r 8dd21c4b0501 -r 6d0af3c10864 src/HOL/Cardinals/Order_Relation_More.thy
--- a/src/HOL/Cardinals/Order_Relation_More.thy	Mon Jan 20 18:24:56 2014 +0100
+++ b/src/HOL/Cardinals/Order_Relation_More.thy	Mon Jan 20 18:24:56 2014 +0100
@@ -173,7 +173,7 @@
     {from NE obtain a where "a \<in> A" by blast
      with * have "x \<in> underS r a" by simp
      hence "x \<in> Field r"
-     using underS_Field[of r a] by auto
+     using underS_Field[of _ r a] by auto
     }
     ultimately show "x \<in> UnderS r A"
     unfolding UnderS_def by auto
diff -r 8dd21c4b0501 -r 6d0af3c10864 src/HOL/Main.thy
--- a/src/HOL/Main.thy	Mon Jan 20 18:24:56 2014 +0100
+++ b/src/HOL/Main.thy	Mon Jan 20 18:24:56 2014 +0100
@@ -18,10 +18,10 @@
   sup (infixl "\<squnion>" 65) and
   Inf ("\<Sqinter>_" [900] 900) and
   Sup ("\<Squnion>_" [900] 900) and
-  ordLeq2 ("<=o") and
-  ordLeq3 ("\<le>o") and
-  ordLess2 ("<o") and
-  ordIso2 ("=o") and
+  ordLeq2 (infix "<=o" 50) and
+  ordLeq3 (infix "\<le>o" 50) and
+  ordLess2 (infix "<o" 50) and
+  ordIso2 (infix "=o" 50) and
   csum (infixr "+c" 65) and
   cprod (infixr "*c" 80) and
   cexp (infixr "^c" 90)