fixed infix syntax;
authorwenzelm
Thu Oct 09 15:03:06 1997 +0200 (1997-10-09)
changeset 382046b255e140dc
parent 3819 5a6a6f18b109
child 3821 151d49052228
fixed infix syntax;
src/HOL/HOL.thy
src/HOL/Ord.thy
src/HOL/Set.thy
     1.1 --- a/src/HOL/HOL.thy	Thu Oct 09 15:01:11 1997 +0200
     1.2 +++ b/src/HOL/HOL.thy	Thu Oct 09 15:03:06 1997 +0200
     1.3 @@ -25,10 +25,6 @@
     1.4    bool :: term
     1.5  
     1.6  
     1.7 -syntax ("" output)
     1.8 -  "op ="        :: ['a, 'a] => bool                 ("(_ =/ _)" [51, 51] 50)
     1.9 -  "op ~="       :: ['a, 'a] => bool                 ("(_ ~=/ _)" [51, 51] 50)
    1.10 -
    1.11  consts
    1.12  
    1.13    (* Constants *)
    1.14 @@ -75,6 +71,7 @@
    1.15    "*"           :: ['a::times, 'a] => 'a            (infixl 70)
    1.16    (*See Nat.thy for "^"*)
    1.17  
    1.18 +
    1.19  (** Additional concrete syntax **)
    1.20  
    1.21  types
    1.22 @@ -116,11 +113,9 @@
    1.23    "_Let (_binds b bs) e"  == "_Let b (_Let bs e)"
    1.24    "let x = a in e"        == "Let a (%x. e)"
    1.25  
    1.26 -syntax (symbols output)
    1.27 -  "op ~="       :: ['a, 'a] => bool                 ("(_ \\<noteq>/ _)" [51, 51] 50)
    1.28 -  "*All"        :: [idts, bool] => bool             ("(3\\<forall>_./ _)" [0, 10] 10)
    1.29 -  "*Ex"         :: [idts, bool] => bool             ("(3\\<exists>_./ _)" [0, 10] 10)
    1.30 -  "*Ex1"        :: [idts, bool] => bool             ("(3\\<exists>!_./ _)" [0, 10] 10)
    1.31 +syntax ("" output)
    1.32 +  "op ="        :: ['a, 'a] => bool                 ("(_ =/ _)" [51, 51] 50)
    1.33 +  "op ~="       :: ['a, 'a] => bool                 ("(_ ~=/ _)" [51, 51] 50)
    1.34  
    1.35  syntax (symbols)
    1.36    Not           :: bool => bool                     ("\\<not> _" [40] 40)
    1.37 @@ -136,6 +131,12 @@
    1.38    "@case1"      :: ['a, 'b] => case_syn             ("(2_ \\<Rightarrow>/ _)" 10)
    1.39  (*"@case2"      :: [case_syn, cases_syn] => cases_syn   ("_/ \\<orelse> _")*)
    1.40  
    1.41 +syntax (symbols output)
    1.42 +  "op ~="       :: ['a, 'a] => bool                 ("(_ \\<noteq>/ _)" [51, 51] 50)
    1.43 +  "*All"        :: [idts, bool] => bool             ("(3\\<forall>_./ _)" [0, 10] 10)
    1.44 +  "*Ex"         :: [idts, bool] => bool             ("(3\\<exists>_./ _)" [0, 10] 10)
    1.45 +  "*Ex1"        :: [idts, bool] => bool             ("(3\\<exists>!_./ _)" [0, 10] 10)
    1.46 +
    1.47  
    1.48  
    1.49  (** Rules and definitions **)
    1.50 @@ -178,8 +179,9 @@
    1.51    o_def         "(f::'b=>'c) o g == (%(x::'a). f(g(x)))"
    1.52    if_def        "If P x y == @z::'a. (P=True --> z=x) & (P=False --> z=y)"
    1.53  
    1.54 -constdefs arbitrary :: 'a
    1.55 -         "arbitrary == @x.False"
    1.56 +consts
    1.57 +  arbitrary :: 'a
    1.58 +
    1.59  
    1.60  end
    1.61  
     2.1 --- a/src/HOL/Ord.thy	Thu Oct 09 15:01:11 1997 +0200
     2.2 +++ b/src/HOL/Ord.thy	Thu Oct 09 15:03:06 1997 +0200
     2.3 @@ -11,6 +11,10 @@
     2.4  axclass
     2.5    ord < term
     2.6  
     2.7 +syntax
     2.8 +  "op <"        :: ['a::ord, 'a] => bool             ("op <")
     2.9 +  "op <="       :: ['a::ord, 'a] => bool             ("op <=")
    2.10 +
    2.11  consts
    2.12    "op <"        :: ['a::ord, 'a] => bool             ("(_/ < _)"  [50, 51] 50)
    2.13    "op <="       :: ['a::ord, 'a] => bool             ("(_/ <= _)" [50, 51] 50)
    2.14 @@ -19,13 +23,10 @@
    2.15  
    2.16    Least         :: ('a::ord=>bool) => 'a             (binder "LEAST " 10)
    2.17  
    2.18 -syntax
    2.19 -  "op <"        :: ['a::ord, 'a] => bool             ("op <")
    2.20 -  "op <="       :: ['a::ord, 'a] => bool             ("op <=")
    2.21 +syntax (symbols)
    2.22 +  "op <="       :: ['a::ord, 'a] => bool             ("op \\<le>")
    2.23 +  "op <="       :: ['a::ord, 'a] => bool             ("(_/ \\<le> _)"  [50, 51] 50)
    2.24  
    2.25 -syntax (symbols)
    2.26 -  "op <="       :: ['a::ord, 'a] => bool             ("(_/ \\<le> _)"  [50, 51] 50)
    2.27 -  "op <="       :: ['a::ord, 'a] => bool             ("op \\<le>")
    2.28  
    2.29  defs
    2.30    mono_def      "mono(f) == (!A B. A <= B --> f(A) <= f(B))"
     3.1 --- a/src/HOL/Set.thy	Thu Oct 09 15:01:11 1997 +0200
     3.2 +++ b/src/HOL/Set.thy	Thu Oct 09 15:03:06 1997 +0200
     3.3 @@ -18,6 +18,9 @@
     3.4  instance
     3.5    set :: (term) {ord, minus, power}
     3.6  
     3.7 +syntax
     3.8 +  "op :"        :: ['a, 'a set] => bool             ("op :")
     3.9 +
    3.10  consts
    3.11    "{}"          :: 'a set                           ("{}")
    3.12    insert        :: ['a, 'a set] => 'a set
    3.13 @@ -42,14 +45,12 @@
    3.14  
    3.15  syntax
    3.16  
    3.17 -  "op :"        :: ['a, 'a set] => bool               ("op :")
    3.18 -
    3.19    UNIV          :: 'a set
    3.20  
    3.21    (* Infix syntax for non-membership *)
    3.22  
    3.23 +  "op ~:"       :: ['a, 'a set] => bool               ("op ~:")
    3.24    "op ~:"       :: ['a, 'a set] => bool               ("(_/ ~: _)" [50, 51] 50)
    3.25 -  "op ~:"       :: ['a, 'a set] => bool               ("op ~:")
    3.26  
    3.27    "@Finset"     :: args => 'a set                     ("{(_)}")
    3.28  
    3.29 @@ -83,22 +84,22 @@
    3.30    "EX x:A. P"   => "Bex A (%x. P)"
    3.31  
    3.32  syntax ("" output)
    3.33 +  "_setle"      :: ['a set, 'a set] => bool           ("op <=")
    3.34    "_setle"      :: ['a set, 'a set] => bool           ("(_/ <= _)" [50, 51] 50)
    3.35 -  "_setle"      :: ['a set, 'a set] => bool           ("op <=")
    3.36 +  "_setless"    :: ['a set, 'a set] => bool           ("op <")
    3.37    "_setless"    :: ['a set, 'a set] => bool           ("(_/ < _)" [50, 51] 50)
    3.38 -  "_setless"    :: ['a set, 'a set] => bool           ("op <")
    3.39  
    3.40  syntax (symbols)
    3.41 +  "_setle"      :: ['a set, 'a set] => bool           ("op \\<subseteq>")
    3.42    "_setle"      :: ['a set, 'a set] => bool           ("(_/ \\<subseteq> _)" [50, 51] 50)
    3.43 -  "_setle"      :: ['a set, 'a set] => bool           ("op \\<subseteq>")
    3.44 +  "_setless"    :: ['a set, 'a set] => bool           ("op \\<subset>")
    3.45    "_setless"    :: ['a set, 'a set] => bool           ("(_/ \\<subset> _)" [50, 51] 50)
    3.46 -  "_setless"    :: ['a set, 'a set] => bool           ("op \\<subset>")
    3.47    "op Int"      :: ['a set, 'a set] => 'a set         (infixl "\\<inter>" 70)
    3.48    "op Un"       :: ['a set, 'a set] => 'a set         (infixl "\\<union>" 65)
    3.49 +  "op :"        :: ['a, 'a set] => bool               ("op \\<in>")
    3.50    "op :"        :: ['a, 'a set] => bool               ("(_/ \\<in> _)" [50, 51] 50)
    3.51 -  "op :"        :: ['a, 'a set] => bool               ("op \\<in>")
    3.52 +  "op ~:"       :: ['a, 'a set] => bool               ("op \\<notin>")
    3.53    "op ~:"       :: ['a, 'a set] => bool               ("(_/ \\<notin> _)" [50, 51] 50)
    3.54 -  "op ~:"       :: ['a, 'a set] => bool               ("op \\<notin>")
    3.55    "UN "         :: [idts, bool] => bool               ("(3\\<Union> _./ _)" 10)
    3.56    "INT "        :: [idts, bool] => bool               ("(3\\<Inter> _./ _)" 10)
    3.57    "@UNION"      :: [pttrn, 'a set, 'b set] => 'b set  ("(3\\<Union> _\\<in>_./ _)" 10)