src/HOL/Set.thy

--- a/src/HOL/Set.thy	Fri Dec 13 17:38:56 1996 +0100
+++ b/src/HOL/Set.thy	Fri Dec 13 17:42:36 1996 +0100
@@ -84,8 +84,13 @@
   "ALL x:A. P"  => "Ball A (%x. P)"
   "EX x:A. P"   => "Bex A (%x. P)"
 
+syntax ("" output)
+  "_setle"      :: ['a set, 'a set] => bool           ("(_/ <= _)" [50, 51] 50)
+  "_setle"      :: ['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>")
   "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)
@@ -140,8 +145,6 @@
   inj_onto_def  "inj_onto f A   == ! x:A. ! y:A. f(x)=f(y) --> x=y"
   surj_def      "surj(f)        == ! y. ? x. y=f(x)"
 
-(* start 8bit 1 *)
-(* end 8bit 1 *)
 
 end
 
@@ -150,6 +153,13 @@
 
 local
 
+(* Set inclusion *)
+
+fun le_tr' (*op <=*) (Type ("fun", (Type ("set", _) :: _))) ts =
+      list_comb (Syntax.const "_setle", ts)
+  | le_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) *)
 
@@ -182,6 +192,7 @@
 
 val parse_translation = [("@SetCompr", setcompr_tr)];
 val print_translation = [("Collect", setcompr_tr')];
+val typed_print_translation = [("op <=", le_tr')];
 val print_ast_translation =
   map HOL.alt_ast_tr' [("@Ball", "*Ball"), ("@Bex", "*Bex")];