src/HOL/HOL.thy
changeset 3248 3e1664348551
parent 3230 3772723c5e41
child 3320 3a5e4930fb77
     1.1 --- a/src/HOL/HOL.thy	Tue May 20 12:14:31 1997 +0200
     1.2 +++ b/src/HOL/HOL.thy	Tue May 20 12:22:33 1997 +0200
     1.3 @@ -116,6 +116,9 @@
     1.4  
     1.5  syntax (symbols output)
     1.6    "op ~="       :: ['a, 'a] => bool                 ("(_ \\<noteq>/ _)" [51, 51] 50)
     1.7 +  "*All"        :: [idts, bool] => bool             ("(3\\<forall>_./ _)" [0, 10] 10)
     1.8 +  "*Ex"         :: [idts, bool] => bool             ("(3\\<exists>_./ _)" [0, 10] 10)
     1.9 +  "*Ex1"        :: [idts, bool] => bool             ("(3\\<exists>!_./ _)" [0, 10] 10)
    1.10  
    1.11  syntax (symbols)
    1.12    Not           :: bool => bool                     ("\\<not> _" [40] 40)
    1.13 @@ -131,12 +134,6 @@
    1.14    "@case1"      :: ['a, 'b] => case_syn             ("(2_ \\<Rightarrow>/ _)" 10)
    1.15  (*"@case2"      :: [case_syn, cases_syn] => cases_syn   ("_/ \\<orelse> _")*)
    1.16  
    1.17 -syntax (symbols output)
    1.18 -  "*All"        :: [idts, bool] => bool             ("(3\\<forall>_./ _)" [0, 10] 10)
    1.19 -  "*Ex"         :: [idts, bool] => bool             ("(3\\<exists>_./ _)" [0, 10] 10)
    1.20 -  "*Ex1"        :: [idts, bool] => bool             ("(3\\<exists>!_./ _)" [0, 10] 10)
    1.21 -
    1.22 -
    1.23  
    1.24  
    1.25  (** Rules and definitions **)