# HG changeset patch
# User wenzelm
# Date 856886245 -3600
# Node ID 9781d63ef06398e937ce56546340406a374b192e
# Parent  be7b439baef24d5a92cc8b12bc19ca2a3003d299
added proper subset symbols syntax;

diff -r be7b439baef2 -r 9781d63ef063 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Tue Feb 25 15:12:49 1997 +0100
+++ b/src/HOL/Set.thy	Tue Feb 25 16:57:25 1997 +0100
@@ -87,10 +87,14 @@
 syntax ("" output)
   "_setle"      :: ['a set, 'a set] => bool           ("(_/ <= _)" [50, 51] 50)
   "_setle"      :: ['a set, 'a set] => bool           ("op <=")
+  "_setless"    :: ['a set, 'a set] => bool           ("(_/ < _)" [50, 51] 50)
+  "_setless"    :: ['a set, 'a set] => bool           ("op <")
 
 syntax (symbols)
   "_setle"      :: ['a set, 'a set] => bool           ("(_/ \\<subseteq> _)" [50, 51] 50)
   "_setle"      :: ['a set, 'a set] => bool           ("op \\<subseteq>")
+  "_setless"    :: ['a set, 'a set] => bool           ("(_/ \\<subset> _)" [50, 51] 50)
+  "_setless"    :: ['a set, 'a set] => bool           ("op \\<subset>")
   "op Int"      :: ['a set, 'a set] => 'a set         (infixl "\\<inter>" 70)
   "op Un"       :: ['a set, 'a set] => 'a set         (infixl "\\<union>" 65)
   "op :"        :: ['a, 'a set] => bool               ("(_/ \\<in> _)" [50, 51] 50)
@@ -112,6 +116,7 @@
 
 translations
   "op \\<subseteq>" => "op <="
+  "op \\<subset>" => "op <"
 
 
 
@@ -161,6 +166,10 @@
       list_comb (Syntax.const "_setle", ts)
   | le_tr' (*op <=*) _ _ = raise Match;
 
+fun less_tr' (*op <*) (Type ("fun", (Type ("set", _) :: _))) ts =
+      list_comb (Syntax.const "_setless", ts)
+  | less_tr' (*op <*) _ _ = raise Match;
+
 
 (* Translates between { e | x1..xn. P} and {u. ? x1..xn. u=e & P}      *)
 (* {y. ? x1..xn. y = e & P} is only translated if [0..n] subset bvs(e) *)
@@ -194,7 +203,7 @@
 
 val parse_translation = [("@SetCompr", setcompr_tr)];
 val print_translation = [("Collect", setcompr_tr')];
-val typed_print_translation = [("op <=", le_tr')];
+val typed_print_translation = [("op <=", le_tr'), ("op <", less_tr')];
 val print_ast_translation =
   map HOL.alt_ast_tr' [("@Ball", "*Ball"), ("@Bex", "*Bex")];