# HG changeset patch
# User wenzelm
# Date 1444508853 -7200
# Node ID 6204c86280ff7f3ba13d602c449e8118175a8bb9
# Parent  ce1b2234cab62301a257b55b04571e69cb8ed765
tuned syntax -- more symbols;

diff -r ce1b2234cab6 -r 6204c86280ff src/ZF/Main_ZF.thy
--- 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"
diff -r ce1b2234cab6 -r 6204c86280ff src/ZF/Ordinal.thy
--- 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)