--- 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
--- 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