| changeset 12620 | 4e6626725e21 |
| parent 9907 | 473a6604da94 |
| child 12720 | f8a134b9a57f |
--- a/src/ZF/OrdQuant.ML Wed Jan 02 21:54:45 2002 +0100 +++ b/src/ZF/OrdQuant.ML Thu Jan 03 17:01:59 2002 +0100 @@ -5,6 +5,10 @@ Quantifiers and union operator for ordinals. *) +val oall_def = thm "oall_def"; +val oex_def = thm "oex_def"; +val OUnion_def = thm "OUnion_def"; + (*** universal quantifier for ordinals ***) val prems = Goalw [oall_def]