# HG changeset patch
# User wenzelm
# Date 1083954770 -7200
# Node ID 7d8d4c9b36fd7d44d0ea7d4e1ecd61a819c5ee88
# Parent  1846cc85ada1ece89d516a2654e35bc35c9fdc90
tuned notation;

diff -r 1846cc85ada1 -r 7d8d4c9b36fd src/HOL/Induct/Ordinals.thy
--- a/src/HOL/Induct/Ordinals.thy	Fri May 07 20:32:40 2004 +0200
+++ b/src/HOL/Induct/Ordinals.thy	Fri May 07 20:32:50 2004 +0200
@@ -64,13 +64,8 @@
   "veblen (Limit f) = \<nabla>(OpLim (\<lambda>n. veblen (f n)))"
 
 constdefs
-  veb :: "ordinal => ordinal"
   "veb a == veblen a Zero"
-
-constdefs
-  epsilon0 :: ordinal    ("\<epsilon>\<^sub>0")
-  "\<epsilon>\<^sub>0 == veb Zero"
-  Gamma0 :: ordinal    ("\<Gamma>\<^sub>0")
-  "\<Gamma>\<^sub>0 == Limit (\<lambda>n. iter veb n Zero)"
+  "\<epsilon>\<^isub>0 == veb Zero"
+  "\<Gamma>\<^isub>0 == Limit (\<lambda>n. iter veb n Zero)"
 
 end
diff -r 1846cc85ada1 -r 7d8d4c9b36fd src/HOL/Induct/Sigma_Algebra.thy
--- a/src/HOL/Induct/Sigma_Algebra.thy	Fri May 07 20:32:40 2004 +0200
+++ b/src/HOL/Induct/Sigma_Algebra.thy	Fri May 07 20:32:50 2004 +0200
@@ -15,7 +15,7 @@
 *}
 
 consts
-  sigma_algebra :: "'a set set => 'a set set"    ("\<sigma>'_algebra")
+  \<sigma>_algebra :: "'a set set => 'a set set"
 
 inductive "\<sigma>_algebra A"
   intros
@@ -32,8 +32,8 @@
 
 theorem sigma_algebra_empty: "{} \<in> \<sigma>_algebra A"
 proof -
-  have "UNIV \<in> \<sigma>_algebra A" by (rule sigma_algebra.UNIV)
-  hence "-UNIV \<in> \<sigma>_algebra A" by (rule sigma_algebra.complement)
+  have "UNIV \<in> \<sigma>_algebra A" by (rule \<sigma>_algebra.UNIV)
+  hence "-UNIV \<in> \<sigma>_algebra A" by (rule \<sigma>_algebra.complement)
   also have "-UNIV = {}" by simp
   finally show ?thesis .
 qed
@@ -42,9 +42,9 @@
   "(!!i::nat. a i \<in> \<sigma>_algebra A) ==> (\<Inter>i. a i) \<in> \<sigma>_algebra A"
 proof -
   assume "!!i::nat. a i \<in> \<sigma>_algebra A"
-  hence "!!i::nat. -(a i) \<in> \<sigma>_algebra A" by (rule sigma_algebra.complement)
-  hence "(\<Union>i. -(a i)) \<in> \<sigma>_algebra A" by (rule sigma_algebra.Union)
-  hence "-(\<Union>i. -(a i)) \<in> \<sigma>_algebra A" by (rule sigma_algebra.complement)
+  hence "!!i::nat. -(a i) \<in> \<sigma>_algebra A" by (rule \<sigma>_algebra.complement)
+  hence "(\<Union>i. -(a i)) \<in> \<sigma>_algebra A" by (rule \<sigma>_algebra.Union)
+  hence "-(\<Union>i. -(a i)) \<in> \<sigma>_algebra A" by (rule \<sigma>_algebra.complement)
   also have "-(\<Union>i. -(a i)) = (\<Inter>i. a i)" by simp
   finally show ?thesis .
 qed