src/ZF/OrdQuant.thy
changeset 14565 c6dc17aab88a
parent 13807 a28a8fbc76d4
child 16417 9bc16273c2d4
     1.1 --- a/src/ZF/OrdQuant.thy	Wed Apr 14 13:28:46 2004 +0200
     1.2 +++ b/src/ZF/OrdQuant.thy	Wed Apr 14 14:13:05 2004 +0200
     1.3 @@ -36,6 +36,10 @@
     1.4    "@oall"     :: "[idt, i, o] => o"        ("(3\<forall>_<_./ _)" 10)
     1.5    "@oex"      :: "[idt, i, o] => o"        ("(3\<exists>_<_./ _)" 10)
     1.6    "@OUNION"   :: "[idt, i, i] => i"        ("(3\<Union>_<_./ _)" 10)
     1.7 +syntax (HTML output)
     1.8 +  "@oall"     :: "[idt, i, o] => o"        ("(3\<forall>_<_./ _)" 10)
     1.9 +  "@oex"      :: "[idt, i, o] => o"        ("(3\<exists>_<_./ _)" 10)
    1.10 +  "@OUNION"   :: "[idt, i, i] => i"        ("(3\<Union>_<_./ _)" 10)
    1.11  
    1.12  
    1.13  subsubsection {*simplification of the new quantifiers*}
    1.14 @@ -204,6 +208,9 @@
    1.15  syntax (xsymbols)
    1.16    "@rall"     :: "[pttrn, i=>o, o] => o"        ("(3\<forall>_[_]./ _)" 10)
    1.17    "@rex"      :: "[pttrn, i=>o, o] => o"        ("(3\<exists>_[_]./ _)" 10)
    1.18 +syntax (HTML output)
    1.19 +  "@rall"     :: "[pttrn, i=>o, o] => o"        ("(3\<forall>_[_]./ _)" 10)
    1.20 +  "@rex"      :: "[pttrn, i=>o, o] => o"        ("(3\<exists>_[_]./ _)" 10)
    1.21  
    1.22  translations
    1.23    "ALL x[M]. P"  == "rall(M, %x. P)"