src/ZF/OrdQuant.thy
changeset 35112 ff6f60e6ab85
parent 32010 cb1a1c94b4cd
child 36543 0e7fc5bf38de
     1.1 --- a/src/ZF/OrdQuant.thy	Thu Feb 11 22:03:37 2010 +0100
     1.2 +++ b/src/ZF/OrdQuant.thy	Thu Feb 11 22:06:37 2010 +0100
     1.3 @@ -23,9 +23,9 @@
     1.4      "OUnion(i,B) == {z: \<Union>x\<in>i. B(x). Ord(i)}"
     1.5  
     1.6  syntax
     1.7 -  "@oall"     :: "[idt, i, o] => o"        ("(3ALL _<_./ _)" 10)
     1.8 -  "@oex"      :: "[idt, i, o] => o"        ("(3EX _<_./ _)" 10)
     1.9 -  "@OUNION"   :: "[idt, i, i] => i"        ("(3UN _<_./ _)" 10)
    1.10 +  "_oall"     :: "[idt, i, o] => o"        ("(3ALL _<_./ _)" 10)
    1.11 +  "_oex"      :: "[idt, i, o] => o"        ("(3EX _<_./ _)" 10)
    1.12 +  "_OUNION"   :: "[idt, i, i] => i"        ("(3UN _<_./ _)" 10)
    1.13  
    1.14  translations
    1.15    "ALL x<a. P"  == "CONST oall(a, %x. P)"
    1.16 @@ -33,13 +33,13 @@
    1.17    "UN x<a. B"   == "CONST OUnion(a, %x. B)"
    1.18  
    1.19  syntax (xsymbols)
    1.20 -  "@oall"     :: "[idt, i, o] => o"        ("(3\<forall>_<_./ _)" 10)
    1.21 -  "@oex"      :: "[idt, i, o] => o"        ("(3\<exists>_<_./ _)" 10)
    1.22 -  "@OUNION"   :: "[idt, i, i] => i"        ("(3\<Union>_<_./ _)" 10)
    1.23 +  "_oall"     :: "[idt, i, o] => o"        ("(3\<forall>_<_./ _)" 10)
    1.24 +  "_oex"      :: "[idt, i, o] => o"        ("(3\<exists>_<_./ _)" 10)
    1.25 +  "_OUNION"   :: "[idt, i, i] => i"        ("(3\<Union>_<_./ _)" 10)
    1.26  syntax (HTML output)
    1.27 -  "@oall"     :: "[idt, i, o] => o"        ("(3\<forall>_<_./ _)" 10)
    1.28 -  "@oex"      :: "[idt, i, o] => o"        ("(3\<exists>_<_./ _)" 10)
    1.29 -  "@OUNION"   :: "[idt, i, i] => i"        ("(3\<Union>_<_./ _)" 10)
    1.30 +  "_oall"     :: "[idt, i, o] => o"        ("(3\<forall>_<_./ _)" 10)
    1.31 +  "_oex"      :: "[idt, i, o] => o"        ("(3\<exists>_<_./ _)" 10)
    1.32 +  "_OUNION"   :: "[idt, i, i] => i"        ("(3\<Union>_<_./ _)" 10)
    1.33  
    1.34  
    1.35  subsubsection {*simplification of the new quantifiers*}
    1.36 @@ -203,15 +203,15 @@
    1.37      "rex(M, P) == EX x. M(x) & P(x)"
    1.38  
    1.39  syntax
    1.40 -  "@rall"     :: "[pttrn, i=>o, o] => o"        ("(3ALL _[_]./ _)" 10)
    1.41 -  "@rex"      :: "[pttrn, i=>o, o] => o"        ("(3EX _[_]./ _)" 10)
    1.42 +  "_rall"     :: "[pttrn, i=>o, o] => o"        ("(3ALL _[_]./ _)" 10)
    1.43 +  "_rex"      :: "[pttrn, i=>o, o] => o"        ("(3EX _[_]./ _)" 10)
    1.44  
    1.45  syntax (xsymbols)
    1.46 -  "@rall"     :: "[pttrn, i=>o, o] => o"        ("(3\<forall>_[_]./ _)" 10)
    1.47 -  "@rex"      :: "[pttrn, i=>o, o] => o"        ("(3\<exists>_[_]./ _)" 10)
    1.48 +  "_rall"     :: "[pttrn, i=>o, o] => o"        ("(3\<forall>_[_]./ _)" 10)
    1.49 +  "_rex"      :: "[pttrn, i=>o, o] => o"        ("(3\<exists>_[_]./ _)" 10)
    1.50  syntax (HTML output)
    1.51 -  "@rall"     :: "[pttrn, i=>o, o] => o"        ("(3\<forall>_[_]./ _)" 10)
    1.52 -  "@rex"      :: "[pttrn, i=>o, o] => o"        ("(3\<exists>_[_]./ _)" 10)
    1.53 +  "_rall"     :: "[pttrn, i=>o, o] => o"        ("(3\<forall>_[_]./ _)" 10)
    1.54 +  "_rex"      :: "[pttrn, i=>o, o] => o"        ("(3\<exists>_[_]./ _)" 10)
    1.55  
    1.56  translations
    1.57    "ALL x[M]. P"  == "CONST rall(M, %x. P)"