--- a/src/ZF/Main_ZF.thy Sat Oct 10 22:23:25 2015 +0200
+++ b/src/ZF/Main_ZF.thy Sat Oct 10 22:27:33 2015 +0200
@@ -14,11 +14,8 @@
"F^(succ(n)) (x) = F(F^n (x))"
definition
- iterates_omega :: "[i=>i,i] => i" where
- "iterates_omega(F,x) == \<Union>n\<in>nat. F^n (x)"
-
-notation (xsymbols)
- iterates_omega ("(_^\<omega> '(_'))" [60,1000] 60)
+ iterates_omega :: "[i=>i,i] => i" ("(_^\<omega> '(_'))" [60,1000] 60) where
+ "F^\<omega> (x) == \<Union>n\<in>nat. F^n (x)"
lemma iterates_triv:
"[| n\<in>nat; F(x) = x |] ==> F^n (x) = x"
--- a/src/ZF/Ordinal.thy Sat Oct 10 22:23:25 2015 +0200
+++ b/src/ZF/Ordinal.thy Sat Oct 10 22:27:33 2015 +0200
@@ -28,11 +28,8 @@
"Limit(i) == Ord(i) & 0<i & (\<forall>y. y<i \<longrightarrow> succ(y)<i)"
abbreviation
- le (infixl "le" 50) where
- "x le y == x < succ(y)"
-
-notation (xsymbols)
- le (infixl "\<le>" 50)
+ le (infixl "\<le>" 50) where
+ "x \<le> y == x < succ(y)"
subsection\<open>Rules for Transset\<close>
@@ -392,7 +389,7 @@
lemma not_lt_imp_le: "[| ~ i<j; Ord(i); Ord(j) |] ==> j \<le> i"
by (rule_tac i = i and j = j in Ord_linear2, auto)
-subsubsection\<open>Some Rewrite Rules for <, le\<close>
+subsubsection\<open>Some Rewrite Rules for <, \<le>\<close>
lemma Ord_mem_iff_lt: "Ord(j) ==> i\<in>j <-> i<j"
by (unfold lt_def, blast)