src/HOL/Set.ML

tuned comment;

(* legacy ML bindings *)

structure Set =
struct
  val thy = the_context ();
  val Ball_def = Ball_def;
  val Bex_def = Bex_def;
  val Collect_mem_eq = Collect_mem_eq;
  val Compl_def = Compl_def;
  val INTER_def = INTER_def;
  val Int_def = Int_def;
  val Inter_def = Inter_def;
  val Pow_def = Pow_def;
  val UNION_def = UNION_def;
  val UNIV_def = UNIV_def;
  val Un_def = Un_def;
  val Union_def = Union_def;
  val empty_def = empty_def;
  val image_def = image_def;
  val insert_def = insert_def;
  val mem_Collect_eq = mem_Collect_eq;
  val psubset_def = psubset_def;
  val set_diff_def = set_diff_def;
  val subset_def = subset_def;
end;