--- 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:
--- 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]
--- 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
--- 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)