# HG changeset patch
# User wenzelm
# Date 864123753 -7200
# Node ID 3e1664348551e8ed9f36d5633de02e62b134cf1c
# Parent  067dc2d0748954088ffa0681f126159f7d5e0552
tuned;

diff -r 067dc2d07489 -r 3e1664348551 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Tue May 20 12:14:31 1997 +0200
+++ b/src/HOL/HOL.thy	Tue May 20 12:22:33 1997 +0200
@@ -116,6 +116,9 @@
 
 syntax (symbols output)
   "op ~="       :: ['a, 'a] => bool                 ("(_ \\<noteq>/ _)" [51, 51] 50)
+  "*All"        :: [idts, bool] => bool             ("(3\\<forall>_./ _)" [0, 10] 10)
+  "*Ex"         :: [idts, bool] => bool             ("(3\\<exists>_./ _)" [0, 10] 10)
+  "*Ex1"        :: [idts, bool] => bool             ("(3\\<exists>!_./ _)" [0, 10] 10)
 
 syntax (symbols)
   Not           :: bool => bool                     ("\\<not> _" [40] 40)
@@ -131,12 +134,6 @@
   "@case1"      :: ['a, 'b] => case_syn             ("(2_ \\<Rightarrow>/ _)" 10)
 (*"@case2"      :: [case_syn, cases_syn] => cases_syn   ("_/ \\<orelse> _")*)
 
-syntax (symbols output)
-  "*All"        :: [idts, bool] => bool             ("(3\\<forall>_./ _)" [0, 10] 10)
-  "*Ex"         :: [idts, bool] => bool             ("(3\\<exists>_./ _)" [0, 10] 10)
-  "*Ex1"        :: [idts, bool] => bool             ("(3\\<exists>!_./ _)" [0, 10] 10)
-
-
 
 
 (** Rules and definitions **)