Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/ZF/OrdQuant.thy
changeset 14565 c6dc17aab88a
parent 13807 a28a8fbc76d4
child 16417 9bc16273c2d4 
--- a/src/ZF/OrdQuant.thy	Wed Apr 14 13:28:46 2004 +0200
+++ b/src/ZF/OrdQuant.thy	Wed Apr 14 14:13:05 2004 +0200
@@ -36,6 +36,10 @@
   "@oall"     :: "[idt, i, o] => o"        ("(3\<forall>_<_./ _)" 10)
   "@oex"      :: "[idt, i, o] => o"        ("(3\<exists>_<_./ _)" 10)
   "@OUNION"   :: "[idt, i, i] => i"        ("(3\<Union>_<_./ _)" 10)
+syntax (HTML output)
+  "@oall"     :: "[idt, i, o] => o"        ("(3\<forall>_<_./ _)" 10)
+  "@oex"      :: "[idt, i, o] => o"        ("(3\<exists>_<_./ _)" 10)
+  "@OUNION"   :: "[idt, i, i] => i"        ("(3\<Union>_<_./ _)" 10)
 
 
 subsubsection {*simplification of the new quantifiers*}
@@ -204,6 +208,9 @@
 syntax (xsymbols)
   "@rall"     :: "[pttrn, i=>o, o] => o"        ("(3\<forall>_[_]./ _)" 10)
   "@rex"      :: "[pttrn, i=>o, o] => o"        ("(3\<exists>_[_]./ _)" 10)
+syntax (HTML output)
+  "@rall"     :: "[pttrn, i=>o, o] => o"        ("(3\<forall>_[_]./ _)" 10)
+  "@rex"      :: "[pttrn, i=>o, o] => o"        ("(3\<exists>_[_]./ _)" 10)
 
 translations
   "ALL x[M]. P"  == "rall(M, %x. P)"
isabelle