# HG changeset patch # User paulson # Date 1025861992 -7200 # Node ID 98ce70e7d1f7149712a13bce8dd180d4f6b55c54 # Parent c505fc950cbe20958ed45056fe12a6910f3e0024 fixed precedences of ** diff -r c505fc950cbe -r 98ce70e7d1f7 src/ZF/OrdQuant.thy --- a/src/ZF/OrdQuant.thy Fri Jul 05 11:18:05 2002 +0200 +++ b/src/ZF/OrdQuant.thy Fri Jul 05 11:39:52 2002 +0200 @@ -38,7 +38,7 @@ "@OUNION" :: "[idt, i, i] => i" ("(3\_<_./ _)" 10) -(** simplification of the new quantifiers **) +subsubsection {*simplification of the new quantifiers*} (*MOST IMPORTANT that this is added to the simpset BEFORE Ord_atomize @@ -60,7 +60,7 @@ apply (blast intro: lt_Ord2) done -(** Union over ordinals **) +subsubsection {*Union over ordinals*} lemma Ord_OUN [intro,simp]: "[| !!x. x Ord(B(x)) |] ==> Ord(\x P(x)) == Trueprop (ALL x P(x) |] ==> ALL x EX x b: (UN z o" ("**_") +constdefs setclass :: "[i,i] => o" ("**_" [40] 40) "setclass(A,x) == x : A" declare setclass_def [simp]