fixed precedences of **
authorpaulson
Fri Jul 05 11:39:52 2002 +0200 (2002-07-05)
changeset 1330298ce70e7d1f7
parent 13301 c505fc950cbe
child 13303 60301202f91b
fixed precedences of **
src/ZF/OrdQuant.thy
     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.31  by (simp add: oall_def)
    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]