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/HOL/Bali/Basis.thy
changeset 35355 613e133966ea
parent 35067 af4c18c30593
child 35417 47ee18b6ae32 
--- a/src/HOL/Bali/Basis.thy	Wed Feb 24 22:04:10 2010 +0100
+++ b/src/HOL/Bali/Basis.thy	Wed Feb 24 22:09:50 2010 +0100
@@ -222,12 +222,12 @@
 section "quantifiers for option type"
 
 syntax
-  Oall :: "[pttrn, 'a option, bool] => bool"   ("(3! _:_:/ _)" [0,0,10] 10)
-  Oex  :: "[pttrn, 'a option, bool] => bool"   ("(3? _:_:/ _)" [0,0,10] 10)
+  "_Oall" :: "[pttrn, 'a option, bool] => bool"   ("(3! _:_:/ _)" [0,0,10] 10)
+  "_Oex"  :: "[pttrn, 'a option, bool] => bool"   ("(3? _:_:/ _)" [0,0,10] 10)
 
 syntax (symbols)
-  Oall :: "[pttrn, 'a option, bool] => bool"   ("(3\<forall>_\<in>_:/ _)"  [0,0,10] 10)
-  Oex  :: "[pttrn, 'a option, bool] => bool"   ("(3\<exists>_\<in>_:/ _)"  [0,0,10] 10)
+  "_Oall" :: "[pttrn, 'a option, bool] => bool"   ("(3\<forall>_\<in>_:/ _)"  [0,0,10] 10)
+  "_Oex"  :: "[pttrn, 'a option, bool] => bool"   ("(3\<exists>_\<in>_:/ _)"  [0,0,10] 10)
 
 translations
   "! x:A: P"    == "! x:CONST Option.set A. P"
isabelle