--- 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
--- 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 ("{(_)}")