src/ZF/OrdQuant.thy
 changeset 13302 98ce70e7d1f7 parent 13298 b4f370679c65 child 13339 0f89104dd377
```     1.1 --- a/src/ZF/OrdQuant.thy	Fri Jul 05 11:18:05 2002 +0200
1.2 +++ b/src/ZF/OrdQuant.thy	Fri Jul 05 11:39:52 2002 +0200
1.3 @@ -38,7 +38,7 @@
1.4    "@OUNION"   :: "[idt, i, i] => i"        ("(3\<Union>_<_./ _)" 10)
1.5
1.6
1.7 -(** simplification of the new quantifiers **)
1.8 +subsubsection {*simplification of the new quantifiers*}
1.9
1.10
1.11  (*MOST IMPORTANT that this is added to the simpset BEFORE Ord_atomize
1.12 @@ -60,7 +60,7 @@
1.13  apply (blast intro: lt_Ord2)
1.14  done
1.15
1.16 -(** Union over ordinals **)
1.17 +subsubsection {*Union over ordinals*}
1.18
1.19  lemma Ord_OUN [intro,simp]:
1.20       "[| !!x. x<A ==> Ord(B(x)) |] ==> Ord(\<Union>x<A. B(x))"
1.21 @@ -109,7 +109,7 @@
1.22       "(!!x. x<A ==> P(x)) == Trueprop (ALL x<A. P(x))"
1.23  by (simp add: oall_def atomize_all atomize_imp)
1.24
1.25 -(*** universal quantifier for ordinals ***)
1.26 +subsubsection {*universal quantifier for ordinals*}
1.27
1.28  lemma oallI [intro!]:
1.29      "[| !!x. x<A ==> P(x) |] ==> ALL x<A. P(x)"
1.30 @@ -138,7 +138,7 @@
1.32
1.33
1.34 -(*** existential quantifier for ordinals ***)
1.35 +subsubsection {*existential quantifier for ordinals*}
1.36
1.37  lemma oexI [intro]:
1.38      "[| P(x);  x<A |] ==> EX x<A. P(x)"
1.39 @@ -163,7 +163,7 @@
1.40  done
1.41
1.42
1.43 -(*** Rules for Ordinal-Indexed Unions ***)
1.44 +subsubsection {*Rules for Ordinal-Indexed Unions*}
1.45
1.46  lemma OUN_I [intro]: "[| a<i;  b: B(a) |] ==> b: (UN z<i. B(z))"
1.47  by (unfold OUnion_def lt_def, blast)
1.48 @@ -335,7 +335,7 @@
1.49
1.50  subsubsection{*Sets as Classes*}
1.51
1.52 -constdefs setclass :: "[i,i] => o"       ("**_")
1.53 +constdefs setclass :: "[i,i] => o"       ("**_" [40] 40)
1.54     "setclass(A,x) == x : A"
1.55
1.56  declare setclass_def [simp]
```