New infix syntax: breaks line BEFORE operator
authorpaulson
Mon Sep 23 17:47:49 1996 +0200 (1996-09-23)
changeset 200672754e060aa2
parent 2005 a52f53caf424
child 2007 968f78b52540
New infix syntax: breaks line BEFORE operator
src/HOL/Ord.thy
src/HOL/Set.thy
     1.1 --- a/src/HOL/Ord.thy	Mon Sep 23 17:46:12 1996 +0200
     1.2 +++ b/src/HOL/Ord.thy	Mon Sep 23 17:47:49 1996 +0200
     1.3 @@ -12,7 +12,8 @@
     1.4    ord < term
     1.5  
     1.6  consts
     1.7 -  "<", "<="     :: ['a::ord, 'a] => bool              (infixl 50)
     1.8 +  "op <"        :: ['a::ord, 'a] => bool             ("(_/ < _)"  [50,51] 50)
     1.9 +  "op <="       :: ['a::ord, 'a] => bool             ("(_/ <= _)" [50,51] 50)
    1.10    mono          :: ['a::ord => 'b::ord] => bool       (*monotonicity*)
    1.11    min, max      :: ['a::ord, 'a] => 'a
    1.12  
     2.1 --- a/src/HOL/Set.thy	Mon Sep 23 17:46:12 1996 +0200
     2.2 +++ b/src/HOL/Set.thy	Mon Sep 23 17:47:49 1996 +0200
     2.3 @@ -32,14 +32,16 @@
     2.4    inj, surj     :: ('a => 'b) => bool                   (*inj/surjective*)
     2.5    inj_onto      :: ['a => 'b, 'a set] => bool
     2.6    "``"          :: ['a => 'b, 'a set] => ('b set)   (infixr 90)
     2.7 -  ":"           :: ['a, 'a set] => bool             (infixl 50) (*membership*)
     2.8 +     (*membership*)
     2.9 +  "op :"        :: ['a, 'a set] => bool             ("(_/ : _)" [50,51] 50)
    2.10  
    2.11  
    2.12  syntax
    2.13  
    2.14    UNIV         :: 'a set
    2.15  
    2.16 -  "~:"          :: ['a, 'a set] => bool             (infixl 50)
    2.17 +     (*infix synatx for non-membership*)
    2.18 +  "op ~:"        :: ['a, 'a set] => bool             ("(_/ ~: _)" [50,51] 50)
    2.19  
    2.20    "@Finset"     :: args => 'a set                   ("{(_)}")
    2.21