src/HOL/Set.thy

  "\<exists>A\<subset>B. P"   =>  "EX A. A \<subset> B & P"
  "\<forall>A\<subseteq>B. P"   =>  "ALL A. A \<subseteq> B --> P"
  "\<exists>A\<subseteq>B. P"   =>  "EX A. A \<subseteq> B & P"
  "\<exists>!A\<subseteq>B. P"  =>  "EX! A. A \<subseteq> B & P"
 
-(* FIXME re-use version in Orderings.thy *)
 print_translation {*
 let
   val thy = the_context ();
   val syntax_name = Sign.const_syntax_name thy;
   val set_type = Sign.intern_type thy "set";