# HG changeset patch
# User paulson
# Date 843493669 -7200
# Node ID 72754e060aa28d9cb32a872893fc271278fbe027
# Parent  a52f53caf4246ebafb5e2d3a31ab05038d377e8c
New infix syntax: breaks line BEFORE operator

diff -r a52f53caf424 -r 72754e060aa2 src/HOL/Ord.thy
--- a/src/HOL/Ord.thy	Mon Sep 23 17:46:12 1996 +0200
+++ b/src/HOL/Ord.thy	Mon Sep 23 17:47:49 1996 +0200
@@ -12,7 +12,8 @@
   ord < term
 
 consts
-  "<", "<="     :: ['a::ord, 'a] => bool              (infixl 50)
+  "op <"        :: ['a::ord, 'a] => bool             ("(_/ < _)"  [50,51] 50)
+  "op <="       :: ['a::ord, 'a] => bool             ("(_/ <= _)" [50,51] 50)
   mono          :: ['a::ord => 'b::ord] => bool       (*monotonicity*)
   min, max      :: ['a::ord, 'a] => 'a
 
diff -r a52f53caf424 -r 72754e060aa2 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Mon Sep 23 17:46:12 1996 +0200
+++ b/src/HOL/Set.thy	Mon Sep 23 17:47:49 1996 +0200
@@ -32,14 +32,16 @@
   inj, surj     :: ('a => 'b) => bool                   (*inj/surjective*)
   inj_onto      :: ['a => 'b, 'a set] => bool
   "``"          :: ['a => 'b, 'a set] => ('b set)   (infixr 90)
-  ":"           :: ['a, 'a set] => bool             (infixl 50) (*membership*)
+     (*membership*)
+  "op :"        :: ['a, 'a set] => bool             ("(_/ : _)" [50,51] 50)
 
 
 syntax
 
   UNIV         :: 'a set
 
-  "~:"          :: ['a, 'a set] => bool             (infixl 50)
+     (*infix synatx for non-membership*)
+  "op ~:"        :: ['a, 'a set] => bool             ("(_/ ~: _)" [50,51] 50)
 
   "@Finset"     :: args => 'a set                   ("{(_)}")