src/HOL/Set.ML
author wenzelm
Sun Oct 28 22:59:12 2001 +0100 (2001-10-28)
changeset 11979 0a3dace545c5
parent 11770 b6bb7a853dd2
child 12257 e3f7d6fb55d7
permissions -rw-r--r--
converted theory "Set";
clasohm@923
     1
wenzelm@11979
     2
(* legacy ML bindings *)
clasohm@923
     3
wenzelm@11979
     4
structure Set =
wenzelm@11979
     5
struct
wenzelm@11979
     6
  val thy = the_context ();
wenzelm@11979
     7
  val Ball_def = Ball_def;
wenzelm@11979
     8
  val Bex_def = Bex_def;
wenzelm@11979
     9
  val Collect_mem_eq = Collect_mem_eq;
wenzelm@11979
    10
  val Compl_def = Compl_def;
wenzelm@11979
    11
  val INTER_def = INTER_def;
wenzelm@11979
    12
  val Int_def = Int_def;
wenzelm@11979
    13
  val Inter_def = Inter_def;
wenzelm@11979
    14
  val Pow_def = Pow_def;
wenzelm@11979
    15
  val UNION_def = UNION_def;
wenzelm@11979
    16
  val UNIV_def = UNIV_def;
wenzelm@11979
    17
  val Un_def = Un_def;
wenzelm@11979
    18
  val Union_def = Union_def;
wenzelm@11979
    19
  val empty_def = empty_def;
wenzelm@11979
    20
  val image_def = image_def;
wenzelm@11979
    21
  val insert_def = insert_def;
wenzelm@11979
    22
  val mem_Collect_eq = mem_Collect_eq;
wenzelm@11979
    23
  val psubset_def = psubset_def;
wenzelm@11979
    24
  val set_diff_def = set_diff_def;
wenzelm@11979
    25
  val subset_def = subset_def;
wenzelm@11979
    26
end;