# HG changeset patch
# User wenzelm
# Date 850728901 -3600
# Node ID 025e80ed698d36d8a61b4ca81897cd8f9c9e6d7f
# Parent  256dbda3df4f028e94a8dd010b7e6f49ce24b2a3
fixed \<subseteq> input;

diff -r 256dbda3df4f -r 025e80ed698d src/HOL/Set.thy
--- a/src/HOL/Set.thy	Mon Dec 16 10:29:30 1996 +0100
+++ b/src/HOL/Set.thy	Mon Dec 16 10:35:01 1996 +0100
@@ -110,6 +110,9 @@
   "*Ball"       :: [pttrn, 'a set, bool] => bool      ("(3\\<forall> _\\<in>_./ _)" [0, 0, 10] 10)
   "*Bex"        :: [pttrn, 'a set, bool] => bool      ("(3\\<exists> _\\<in>_./ _)" [0, 0, 10] 10)
 
+translations
+  "op \\<subseteq>" => "op <="
+
 
 
 (** Rules and definitions **)