src/HOL/Set.ML
author webertj
Mon Mar 07 19:30:53 2005 +0100 (2005-03-07)
changeset 15584 3478bb4f93ff
parent 13653 ef123b9e8089
child 18413 50c0c118e96d
permissions -rw-r--r--
refute_params: default value itself=1 added (for type classes)
clasohm@923
     1
wenzelm@11979
     2
(* legacy ML bindings *)
clasohm@923
     3
wenzelm@12897
     4
val Ball_def = thm "Ball_def";
wenzelm@12897
     5
val Bex_def = thm "Bex_def";
wenzelm@12897
     6
val CollectD = thm "CollectD";
wenzelm@12897
     7
val CollectE = thm "CollectE";
wenzelm@12897
     8
val CollectI = thm "CollectI";
wenzelm@12897
     9
val Collect_all_eq = thm "Collect_all_eq";
wenzelm@12897
    10
val Collect_ball_eq = thm "Collect_ball_eq";
wenzelm@12897
    11
val Collect_bex_eq = thm "Collect_bex_eq";
wenzelm@12897
    12
val Collect_cong = thm "Collect_cong";
wenzelm@12897
    13
val Collect_conj_eq = thm "Collect_conj_eq";
wenzelm@12897
    14
val Collect_const = thm "Collect_const";
wenzelm@12897
    15
val Collect_disj_eq = thm "Collect_disj_eq";
wenzelm@12897
    16
val Collect_empty_eq = thm "Collect_empty_eq";
wenzelm@12897
    17
val Collect_ex_eq = thm "Collect_ex_eq";
wenzelm@12897
    18
val Collect_mem_eq = thm "Collect_mem_eq";
wenzelm@12897
    19
val Collect_mono = thm "Collect_mono";
wenzelm@12897
    20
val Collect_neg_eq = thm "Collect_neg_eq";
wenzelm@12897
    21
val ComplD = thm "ComplD";
wenzelm@12897
    22
val ComplE = thm "ComplE";
wenzelm@12897
    23
val ComplI = thm "ComplI";
wenzelm@12897
    24
val Compl_Diff_eq = thm "Compl_Diff_eq";
wenzelm@12897
    25
val Compl_INT = thm "Compl_INT";
wenzelm@12897
    26
val Compl_Int = thm "Compl_Int";
wenzelm@12897
    27
val Compl_UN = thm "Compl_UN";
wenzelm@12897
    28
val Compl_UNIV_eq = thm "Compl_UNIV_eq";
wenzelm@12897
    29
val Compl_Un = thm "Compl_Un";
wenzelm@12897
    30
val Compl_anti_mono = thm "Compl_anti_mono";
wenzelm@12897
    31
val Compl_def = thm "Compl_def";
wenzelm@12897
    32
val Compl_disjoint = thm "Compl_disjoint";
wenzelm@12897
    33
val Compl_disjoint2 = thm "Compl_disjoint2";
wenzelm@12897
    34
val Compl_empty_eq = thm "Compl_empty_eq";
wenzelm@12897
    35
val Compl_eq_Compl_iff = thm "Compl_eq_Compl_iff";
wenzelm@12897
    36
val Compl_iff = thm "Compl_iff";
wenzelm@12897
    37
val Compl_partition = thm "Compl_partition";
wenzelm@12897
    38
val Compl_subset_Compl_iff = thm "Compl_subset_Compl_iff";
wenzelm@12897
    39
val DiffD1 = thm "DiffD1";
wenzelm@12897
    40
val DiffD2 = thm "DiffD2";
wenzelm@12897
    41
val DiffE = thm "DiffE";
wenzelm@12897
    42
val DiffI = thm "DiffI";
wenzelm@12897
    43
val Diff_Compl = thm "Diff_Compl";
wenzelm@12897
    44
val Diff_Int = thm "Diff_Int";
wenzelm@12897
    45
val Diff_Int_distrib = thm "Diff_Int_distrib";
wenzelm@12897
    46
val Diff_Int_distrib2 = thm "Diff_Int_distrib2";
wenzelm@12897
    47
val Diff_UNIV = thm "Diff_UNIV";
wenzelm@12897
    48
val Diff_Un = thm "Diff_Un";
wenzelm@12897
    49
val Diff_cancel = thm "Diff_cancel";
wenzelm@12897
    50
val Diff_disjoint = thm "Diff_disjoint";
wenzelm@12897
    51
val Diff_empty = thm "Diff_empty";
wenzelm@12897
    52
val Diff_eq = thm "Diff_eq";
wenzelm@12897
    53
val Diff_eq_empty_iff = thm "Diff_eq_empty_iff";
wenzelm@12897
    54
val Diff_iff = thm "Diff_iff";
wenzelm@12897
    55
val Diff_insert = thm "Diff_insert";
wenzelm@12897
    56
val Diff_insert0 = thm "Diff_insert0";
wenzelm@12897
    57
val Diff_insert2 = thm "Diff_insert2";
wenzelm@12897
    58
val Diff_insert_absorb = thm "Diff_insert_absorb";
wenzelm@12897
    59
val Diff_mono = thm "Diff_mono";
wenzelm@12897
    60
val Diff_partition = thm "Diff_partition";
wenzelm@12897
    61
val Diff_subset = thm "Diff_subset";
wenzelm@12897
    62
val Diff_triv = thm "Diff_triv";
wenzelm@12897
    63
val INTER_def = thm "INTER_def";
wenzelm@12897
    64
val INT_D = thm "INT_D";
wenzelm@12897
    65
val INT_E = thm "INT_E";
wenzelm@12897
    66
val INT_I = thm "INT_I";
wenzelm@12897
    67
val INT_Int_distrib = thm "INT_Int_distrib";
wenzelm@12897
    68
val INT_Un = thm "INT_Un";
wenzelm@12897
    69
val INT_absorb = thm "INT_absorb";
wenzelm@12897
    70
val INT_anti_mono = thm "INT_anti_mono";
wenzelm@12897
    71
val INT_bool_eq = thm "INT_bool_eq";
wenzelm@12897
    72
val INT_cong = thm "INT_cong";
wenzelm@12897
    73
val INT_constant = thm "INT_constant";
wenzelm@12897
    74
val INT_empty = thm "INT_empty";
wenzelm@12897
    75
val INT_eq = thm "INT_eq";
wenzelm@12897
    76
val INT_greatest = thm "INT_greatest";
wenzelm@12897
    77
val INT_iff = thm "INT_iff";
wenzelm@12897
    78
val INT_insert = thm "INT_insert";
wenzelm@12897
    79
val INT_insert_distrib = thm "INT_insert_distrib";
wenzelm@12897
    80
val INT_lower = thm "INT_lower";
wenzelm@12897
    81
val INT_simps = thms "INT_simps";
wenzelm@12897
    82
val INT_subset_iff = thm "INT_subset_iff";
wenzelm@12897
    83
val IntD1 = thm "IntD1";
wenzelm@12897
    84
val IntD2 = thm "IntD2";
wenzelm@12897
    85
val IntE = thm "IntE";
wenzelm@12897
    86
val IntI = thm "IntI";
wenzelm@12897
    87
val Int_Collect = thm "Int_Collect";
wenzelm@12897
    88
val Int_Collect_mono = thm "Int_Collect_mono";
wenzelm@12897
    89
val Int_Diff = thm "Int_Diff";
wenzelm@12897
    90
val Int_Inter_image = thm "Int_Inter_image";
wenzelm@12897
    91
val Int_UNIV = thm "Int_UNIV";
wenzelm@12897
    92
val Int_UNIV_left = thm "Int_UNIV_left";
wenzelm@12897
    93
val Int_UNIV_right = thm "Int_UNIV_right";
wenzelm@12897
    94
val Int_UN_distrib = thm "Int_UN_distrib";
wenzelm@12897
    95
val Int_UN_distrib2 = thm "Int_UN_distrib2";
wenzelm@12897
    96
val Int_Un_distrib = thm "Int_Un_distrib";
wenzelm@12897
    97
val Int_Un_distrib2 = thm "Int_Un_distrib2";
wenzelm@12897
    98
val Int_Union = thm "Int_Union";
wenzelm@12897
    99
val Int_Union2 = thm "Int_Union2";
wenzelm@12897
   100
val Int_absorb = thm "Int_absorb";
wenzelm@12897
   101
val Int_absorb1 = thm "Int_absorb1";
wenzelm@12897
   102
val Int_absorb2 = thm "Int_absorb2";
wenzelm@12897
   103
val Int_ac = thms "Int_ac";
wenzelm@12897
   104
val Int_assoc = thm "Int_assoc";
wenzelm@12897
   105
val Int_commute = thm "Int_commute";
wenzelm@12897
   106
val Int_def = thm "Int_def";
wenzelm@12897
   107
val Int_empty_left = thm "Int_empty_left";
wenzelm@12897
   108
val Int_empty_right = thm "Int_empty_right";
wenzelm@12897
   109
val Int_eq_Inter = thm "Int_eq_Inter";
wenzelm@12897
   110
val Int_greatest = thm "Int_greatest";
wenzelm@12897
   111
val Int_iff = thm "Int_iff";
wenzelm@12897
   112
val Int_insert_left = thm "Int_insert_left";
wenzelm@12897
   113
val Int_insert_right = thm "Int_insert_right";
wenzelm@12897
   114
val Int_left_absorb = thm "Int_left_absorb";
wenzelm@12897
   115
val Int_left_commute = thm "Int_left_commute";
wenzelm@12897
   116
val Int_lower1 = thm "Int_lower1";
wenzelm@12897
   117
val Int_lower2 = thm "Int_lower2";
wenzelm@12897
   118
val Int_mono = thm "Int_mono";
wenzelm@12897
   119
val Int_subset_iff = thm "Int_subset_iff";
wenzelm@12897
   120
val InterD = thm "InterD";
wenzelm@12897
   121
val InterE = thm "InterE";
wenzelm@12897
   122
val InterI = thm "InterI";
wenzelm@12897
   123
val Inter_UNIV = thm "Inter_UNIV";
wenzelm@12897
   124
val Inter_Un_distrib = thm "Inter_Un_distrib";
wenzelm@12897
   125
val Inter_Un_subset = thm "Inter_Un_subset";
wenzelm@12897
   126
val Inter_anti_mono = thm "Inter_anti_mono";
wenzelm@12897
   127
val Inter_def = thm "Inter_def";
wenzelm@12897
   128
val Inter_empty = thm "Inter_empty";
wenzelm@12897
   129
val Inter_greatest = thm "Inter_greatest";
wenzelm@12897
   130
val Inter_iff = thm "Inter_iff";
wenzelm@12897
   131
val Inter_image_eq = thm "Inter_image_eq";
wenzelm@12897
   132
val Inter_insert = thm "Inter_insert";
wenzelm@12897
   133
val Inter_lower = thm "Inter_lower";
wenzelm@12897
   134
val PowD = thm "PowD";
wenzelm@12897
   135
val PowI = thm "PowI";
wenzelm@12897
   136
val Pow_Compl = thm "Pow_Compl";
wenzelm@12897
   137
val Pow_INT_eq = thm "Pow_INT_eq";
wenzelm@12897
   138
val Pow_Int_eq = thm "Pow_Int_eq";
wenzelm@12897
   139
val Pow_UNIV = thm "Pow_UNIV";
wenzelm@12897
   140
val Pow_bottom = thm "Pow_bottom";
wenzelm@12897
   141
val Pow_def = thm "Pow_def";
wenzelm@12897
   142
val Pow_empty = thm "Pow_empty";
wenzelm@12897
   143
val Pow_iff = thm "Pow_iff";
wenzelm@12897
   144
val Pow_insert = thm "Pow_insert";
wenzelm@12897
   145
val Pow_mono = thm "Pow_mono";
wenzelm@12897
   146
val Pow_top = thm "Pow_top";
wenzelm@12897
   147
val UNION_def = thm "UNION_def";
wenzelm@12897
   148
val UNIV_I = thm "UNIV_I";
wenzelm@12897
   149
val UNIV_def = thm "UNIV_def";
wenzelm@12897
   150
val UNIV_not_empty = thm "UNIV_not_empty";
wenzelm@12897
   151
val UNIV_witness = thm "UNIV_witness";
wenzelm@12897
   152
val UN_E = thm "UN_E";
wenzelm@12897
   153
val UN_I = thm "UN_I";
wenzelm@12897
   154
val UN_Pow_subset = thm "UN_Pow_subset";
wenzelm@12897
   155
val UN_UN_flatten = thm "UN_UN_flatten";
wenzelm@12897
   156
val UN_Un = thm "UN_Un";
wenzelm@12897
   157
val UN_Un_distrib = thm "UN_Un_distrib";
wenzelm@12897
   158
val UN_absorb = thm "UN_absorb";
wenzelm@12897
   159
val UN_bool_eq = thm "UN_bool_eq";
wenzelm@12897
   160
val UN_cong = thm "UN_cong";
wenzelm@12897
   161
val UN_constant = thm "UN_constant";
wenzelm@12897
   162
val UN_empty = thm "UN_empty";
wenzelm@12897
   163
val UN_empty2 = thm "UN_empty2";
wenzelm@12897
   164
val UN_eq = thm "UN_eq";
wenzelm@12897
   165
val UN_iff = thm "UN_iff";
wenzelm@12897
   166
val UN_insert = thm "UN_insert";
wenzelm@12897
   167
val UN_insert_distrib = thm "UN_insert_distrib";
wenzelm@12897
   168
val UN_least = thm "UN_least";
wenzelm@12897
   169
val UN_mono = thm "UN_mono";
wenzelm@12897
   170
val UN_simps = thms "UN_simps";
wenzelm@12897
   171
val UN_singleton = thm "UN_singleton";
wenzelm@12897
   172
val UN_subset_iff = thm "UN_subset_iff";
wenzelm@12897
   173
val UN_upper = thm "UN_upper";
wenzelm@12897
   174
val UnCI = thm "UnCI";
wenzelm@12897
   175
val UnE = thm "UnE";
wenzelm@12897
   176
val UnI1 = thm "UnI1";
wenzelm@12897
   177
val UnI2 = thm "UnI2";
wenzelm@12897
   178
val Un_Diff = thm "Un_Diff";
wenzelm@12897
   179
val Un_Diff_Int = thm "Un_Diff_Int";
wenzelm@12897
   180
val Un_Diff_cancel = thm "Un_Diff_cancel";
wenzelm@12897
   181
val Un_Diff_cancel2 = thm "Un_Diff_cancel2";
wenzelm@12897
   182
val Un_INT_distrib = thm "Un_INT_distrib";
wenzelm@12897
   183
val Un_INT_distrib2 = thm "Un_INT_distrib2";
wenzelm@12897
   184
val Un_Int_assoc_eq = thm "Un_Int_assoc_eq";
wenzelm@12897
   185
val Un_Int_crazy = thm "Un_Int_crazy";
wenzelm@12897
   186
val Un_Int_distrib = thm "Un_Int_distrib";
wenzelm@12897
   187
val Un_Int_distrib2 = thm "Un_Int_distrib2";
wenzelm@12897
   188
val Un_Inter = thm "Un_Inter";
wenzelm@12897
   189
val Un_Pow_subset = thm "Un_Pow_subset";
wenzelm@12897
   190
val Un_UNIV_left = thm "Un_UNIV_left";
wenzelm@12897
   191
val Un_UNIV_right = thm "Un_UNIV_right";
wenzelm@12897
   192
val Un_Union_image = thm "Un_Union_image";
wenzelm@12897
   193
val Un_absorb = thm "Un_absorb";
wenzelm@12897
   194
val Un_absorb1 = thm "Un_absorb1";
wenzelm@12897
   195
val Un_absorb2 = thm "Un_absorb2";
wenzelm@12897
   196
val Un_ac = thms "Un_ac";
wenzelm@12897
   197
val Un_assoc = thm "Un_assoc";
wenzelm@12897
   198
val Un_commute = thm "Un_commute";
wenzelm@12897
   199
val Un_def = thm "Un_def";
wenzelm@12897
   200
val Un_empty = thm "Un_empty";
wenzelm@12897
   201
val Un_empty_left = thm "Un_empty_left";
wenzelm@12897
   202
val Un_empty_right = thm "Un_empty_right";
wenzelm@12897
   203
val Un_eq_UN = thm "Un_eq_UN";
wenzelm@12897
   204
val Un_eq_Union = thm "Un_eq_Union";
wenzelm@12897
   205
val Un_iff = thm "Un_iff";
wenzelm@12897
   206
val Un_insert_left = thm "Un_insert_left";
wenzelm@12897
   207
val Un_insert_right = thm "Un_insert_right";
wenzelm@12897
   208
val Un_least = thm "Un_least";
wenzelm@12897
   209
val Un_left_absorb = thm "Un_left_absorb";
wenzelm@12897
   210
val Un_left_commute = thm "Un_left_commute";
wenzelm@12897
   211
val Un_mono = thm "Un_mono";
wenzelm@12897
   212
val Un_subset_iff = thm "Un_subset_iff";
wenzelm@12897
   213
val Un_upper1 = thm "Un_upper1";
wenzelm@12897
   214
val Un_upper2 = thm "Un_upper2";
wenzelm@12897
   215
val UnionE = thm "UnionE";
wenzelm@12897
   216
val UnionI = thm "UnionI";
wenzelm@12897
   217
val Union_Int_subset = thm "Union_Int_subset";
wenzelm@12897
   218
val Union_Pow_eq = thm "Union_Pow_eq";
wenzelm@12897
   219
val Union_UNIV = thm "Union_UNIV";
wenzelm@12897
   220
val Union_Un_distrib = thm "Union_Un_distrib";
wenzelm@12897
   221
val Union_def = thm "Union_def";
wenzelm@12897
   222
val Union_disjoint = thm "Union_disjoint";
wenzelm@12897
   223
val Union_empty = thm "Union_empty";
wenzelm@12897
   224
val Union_empty_conv = thm "Union_empty_conv";
wenzelm@12897
   225
val Union_iff = thm "Union_iff";
wenzelm@12897
   226
val Union_image_eq = thm "Union_image_eq";
wenzelm@12897
   227
val Union_insert = thm "Union_insert";
wenzelm@12897
   228
val Union_least = thm "Union_least";
wenzelm@12897
   229
val Union_mono = thm "Union_mono";
wenzelm@12897
   230
val Union_upper = thm "Union_upper";
wenzelm@12897
   231
val all_bool_eq = thm "all_bool_eq";
wenzelm@12897
   232
val all_mono = thm "all_mono";
wenzelm@12897
   233
val all_not_in_conv = thm "all_not_in_conv";
wenzelm@12897
   234
val atomize_ball = thm "atomize_ball";
wenzelm@12897
   235
val ballE = thm "ballE";
wenzelm@12897
   236
val ballI = thm "ballI";
wenzelm@12897
   237
val ball_UN = thm "ball_UN";
wenzelm@12897
   238
val ball_UNIV = thm "ball_UNIV";
wenzelm@12897
   239
val ball_Un = thm "ball_Un";
wenzelm@12897
   240
val ball_cong = thm "ball_cong";
wenzelm@12897
   241
val ball_conj_distrib = thm "ball_conj_distrib";
wenzelm@12897
   242
val ball_empty = thm "ball_empty";
wenzelm@12897
   243
val ball_one_point1 = thm "ball_one_point1";
wenzelm@12897
   244
val ball_one_point2 = thm "ball_one_point2";
wenzelm@12897
   245
val ball_simps = thms "ball_simps";
wenzelm@12897
   246
val ball_triv = thm "ball_triv";
wenzelm@12897
   247
val basic_monos = thms "basic_monos";
wenzelm@12897
   248
val bexCI = thm "bexCI";
wenzelm@12897
   249
val bexE = thm "bexE";
wenzelm@12897
   250
val bexI = thm "bexI";
wenzelm@12897
   251
val bex_UN = thm "bex_UN";
wenzelm@12897
   252
val bex_UNIV = thm "bex_UNIV";
wenzelm@12897
   253
val bex_Un = thm "bex_Un";
wenzelm@12897
   254
val bex_cong = thm "bex_cong";
wenzelm@12897
   255
val bex_disj_distrib = thm "bex_disj_distrib";
wenzelm@12897
   256
val bex_empty = thm "bex_empty";
wenzelm@12897
   257
val bex_one_point1 = thm "bex_one_point1";
wenzelm@12897
   258
val bex_one_point2 = thm "bex_one_point2";
wenzelm@12897
   259
val bex_simps = thms "bex_simps";
wenzelm@12897
   260
val bex_triv = thm "bex_triv";
wenzelm@12897
   261
val bex_triv_one_point1 = thm "bex_triv_one_point1";
wenzelm@12897
   262
val bex_triv_one_point2 = thm "bex_triv_one_point2";
wenzelm@12897
   263
val bool_induct = thm "bool_induct";
wenzelm@12897
   264
val bspec = thm "bspec";
wenzelm@12897
   265
val conj_mono = thm "conj_mono";
wenzelm@12897
   266
val contra_subsetD = thm "contra_subsetD";
wenzelm@12897
   267
val diff_single_insert = thm "diff_single_insert";
wenzelm@12897
   268
val disj_mono = thm "disj_mono";
wenzelm@12897
   269
val disjoint_eq_subset_Compl = thm "disjoint_eq_subset_Compl";
wenzelm@12897
   270
val disjoint_iff_not_equal = thm "disjoint_iff_not_equal";
wenzelm@12897
   271
val distinct_lemma = thm "distinct_lemma";
wenzelm@12897
   272
val double_complement = thm "double_complement";
wenzelm@12897
   273
val double_diff = thm "double_diff";
wenzelm@12897
   274
val emptyE = thm "emptyE";
wenzelm@12897
   275
val empty_Diff = thm "empty_Diff";
wenzelm@12897
   276
val empty_def = thm "empty_def";
wenzelm@12897
   277
val empty_iff = thm "empty_iff";
wenzelm@12897
   278
val empty_subsetI = thm "empty_subsetI";
wenzelm@12897
   279
val eq_to_mono = thm "eq_to_mono";
wenzelm@12897
   280
val eq_to_mono2 = thm "eq_to_mono2";
wenzelm@12897
   281
val eqset_imp_iff = thm "eqset_imp_iff";
wenzelm@12897
   282
val equalityCE = thm "equalityCE";
wenzelm@12897
   283
val equalityD1 = thm "equalityD1";
wenzelm@12897
   284
val equalityD2 = thm "equalityD2";
wenzelm@12897
   285
val equalityE = thm "equalityE";
wenzelm@12897
   286
val equalityI = thm "equalityI";
wenzelm@12897
   287
val equals0D = thm "equals0D";
wenzelm@12897
   288
val equals0I = thm "equals0I";
wenzelm@12897
   289
val ex_bool_eq = thm "ex_bool_eq";
wenzelm@12897
   290
val ex_mono = thm "ex_mono";
wenzelm@12897
   291
val full_SetCompr_eq = thm "full_SetCompr_eq";
wenzelm@12897
   292
val if_image_distrib = thm "if_image_distrib";
wenzelm@12897
   293
val imageE = thm "imageE";
wenzelm@12897
   294
val imageI = thm "imageI";
wenzelm@12897
   295
val image_Collect = thm "image_Collect";
wenzelm@12897
   296
val image_Un = thm "image_Un";
wenzelm@12897
   297
val image_Union = thm "image_Union";
wenzelm@12897
   298
val image_cong = thm "image_cong";
wenzelm@12897
   299
val image_constant = thm "image_constant";
wenzelm@12897
   300
val image_def = thm "image_def";
wenzelm@12897
   301
val image_empty = thm "image_empty";
wenzelm@12897
   302
val image_eqI = thm "image_eqI";
wenzelm@12897
   303
val image_iff = thm "image_iff";
wenzelm@12897
   304
val image_image = thm "image_image";
wenzelm@12897
   305
val image_insert = thm "image_insert";
wenzelm@12897
   306
val image_is_empty = thm "image_is_empty";
wenzelm@12897
   307
val image_mono = thm "image_mono";
wenzelm@12897
   308
val image_subsetI = thm "image_subsetI";
wenzelm@12897
   309
val image_subset_iff = thm "image_subset_iff";
wenzelm@12897
   310
val imp_mono = thm "imp_mono";
wenzelm@12897
   311
val imp_refl = thm "imp_refl";
wenzelm@12897
   312
val in_mono = thm "in_mono";
wenzelm@12897
   313
val insertCI = thm "insertCI";
wenzelm@12897
   314
val insertE = thm "insertE";
wenzelm@12897
   315
val insertI1 = thm "insertI1";
wenzelm@12897
   316
val insertI2 = thm "insertI2";
wenzelm@12897
   317
val insert_Collect = thm "insert_Collect";
wenzelm@12897
   318
val insert_Diff = thm "insert_Diff";
wenzelm@12897
   319
val insert_Diff1 = thm "insert_Diff1";
wenzelm@12897
   320
val insert_Diff_if = thm "insert_Diff_if";
wenzelm@12897
   321
val insert_absorb = thm "insert_absorb";
wenzelm@12897
   322
val insert_absorb2 = thm "insert_absorb2";
wenzelm@12897
   323
val insert_commute = thm "insert_commute";
wenzelm@12897
   324
val insert_def = thm "insert_def";
wenzelm@12897
   325
val insert_iff = thm "insert_iff";
wenzelm@12897
   326
val insert_image = thm "insert_image";
wenzelm@12897
   327
val insert_is_Un = thm "insert_is_Un";
wenzelm@12897
   328
val insert_mono = thm "insert_mono";
wenzelm@12897
   329
val insert_not_empty = thm "insert_not_empty";
wenzelm@12897
   330
val insert_subset = thm "insert_subset";
wenzelm@12897
   331
val mem_Collect_eq = thm "mem_Collect_eq";
wenzelm@12897
   332
val mem_simps = thms "mem_simps";
wenzelm@12897
   333
val mk_disjoint_insert = thm "mk_disjoint_insert";
wenzelm@12897
   334
val mono_Int = thm "mono_Int";
wenzelm@12897
   335
val mono_Un = thm "mono_Un";
wenzelm@12897
   336
val not_psubset_empty = thm "not_psubset_empty";
wenzelm@12897
   337
val psubsetI = thm "psubsetI";
wenzelm@12897
   338
val psubset_def = thm "psubset_def";
wenzelm@12897
   339
val psubset_eq = thm "psubset_eq";
wenzelm@12897
   340
val psubset_imp_ex_mem = thm "psubset_imp_ex_mem";
wenzelm@12897
   341
val psubset_imp_subset = thm "psubset_imp_subset";
wenzelm@12897
   342
val psubset_insert_iff = thm "psubset_insert_iff";
wenzelm@12897
   343
val psubset_subset_trans = thm "psubset_subset_trans";
wenzelm@12897
   344
val rangeE = thm "rangeE";
wenzelm@12897
   345
val rangeI = thm "rangeI";
wenzelm@12897
   346
val range_composition = thm "range_composition";
wenzelm@12897
   347
val range_eqI = thm "range_eqI";
wenzelm@12897
   348
val rev_bexI = thm "rev_bexI";
wenzelm@12897
   349
val rev_image_eqI = thm "rev_image_eqI";
wenzelm@12897
   350
val rev_subsetD = thm "rev_subsetD";
wenzelm@12897
   351
val set_diff_def = thm "set_diff_def";
wenzelm@12897
   352
val set_eq_subset = thm "set_eq_subset";
wenzelm@12897
   353
val set_ext = thm "set_ext";
wenzelm@12897
   354
val setup_induction = thm "setup_induction";
wenzelm@12897
   355
val singletonD = thm "singletonD";
wenzelm@12897
   356
val singletonE = thm "singletonE";
wenzelm@12897
   357
val singletonI = thm "singletonI";
wenzelm@12897
   358
val singleton_conv = thm "singleton_conv";
wenzelm@12897
   359
val singleton_conv2 = thm "singleton_conv2";
wenzelm@12897
   360
val singleton_iff = thm "singleton_iff";
wenzelm@12897
   361
val singleton_inject = thm "singleton_inject";
wenzelm@12897
   362
val singleton_insert_inj_eq = thm "singleton_insert_inj_eq";
wenzelm@12897
   363
val singleton_insert_inj_eq' = thm "singleton_insert_inj_eq'";
wenzelm@12897
   364
val split_if_eq1 = thm "split_if_eq1";
wenzelm@12897
   365
val split_if_eq2 = thm "split_if_eq2";
wenzelm@12897
   366
val split_if_mem1 = thm "split_if_mem1";
wenzelm@12897
   367
val split_if_mem2 = thm "split_if_mem2";
wenzelm@12897
   368
val split_ifs = thms "split_ifs";
wenzelm@12897
   369
val strip = thms "strip";
wenzelm@12897
   370
val subsetCE = thm "subsetCE";
wenzelm@12897
   371
val subsetD = thm "subsetD";
wenzelm@12897
   372
val subsetI = thm "subsetI";
wenzelm@12897
   373
val subset_Compl_self_eq = thm "subset_Compl_self_eq";
wenzelm@12897
   374
val subset_Pow_Union = thm "subset_Pow_Union";
wenzelm@12897
   375
val subset_UNIV = thm "subset_UNIV";
wenzelm@12897
   376
val subset_Un_eq = thm "subset_Un_eq";
wenzelm@12897
   377
val subset_antisym = thm "subset_antisym";
wenzelm@12897
   378
val subset_def = thm "subset_def";
wenzelm@12897
   379
val subset_empty = thm "subset_empty";
wenzelm@12897
   380
val subset_iff = thm "subset_iff";
wenzelm@12897
   381
val subset_iff_psubset_eq = thm "subset_iff_psubset_eq";
wenzelm@12897
   382
val subset_image_iff = thm "subset_image_iff";
wenzelm@12897
   383
val subset_insert = thm "subset_insert";
wenzelm@12897
   384
val subset_insertI = thm "subset_insertI";
wenzelm@12897
   385
val subset_insert_iff = thm "subset_insert_iff";
wenzelm@12897
   386
val subset_psubset_trans = thm "subset_psubset_trans";
wenzelm@12897
   387
val subset_refl = thm "subset_refl";
wenzelm@12897
   388
val subset_singletonD = thm "subset_singletonD";
wenzelm@12897
   389
val subset_trans = thm "subset_trans";
wenzelm@12897
   390
val vimageD = thm "vimageD";
wenzelm@12897
   391
val vimageE = thm "vimageE";
wenzelm@12897
   392
val vimageI = thm "vimageI";
wenzelm@12897
   393
val vimageI2 = thm "vimageI2";
wenzelm@12897
   394
val vimage_Collect = thm "vimage_Collect";
wenzelm@12897
   395
val vimage_Collect_eq = thm "vimage_Collect_eq";
wenzelm@12897
   396
val vimage_Compl = thm "vimage_Compl";
wenzelm@12897
   397
val vimage_Diff = thm "vimage_Diff";
wenzelm@12897
   398
val vimage_INT = thm "vimage_INT";
wenzelm@12897
   399
val vimage_Int = thm "vimage_Int";
wenzelm@12897
   400
val vimage_UN = thm "vimage_UN";
wenzelm@12897
   401
val vimage_UNIV = thm "vimage_UNIV";
wenzelm@12897
   402
val vimage_Un = thm "vimage_Un";
wenzelm@12897
   403
val vimage_Union = thm "vimage_Union";
wenzelm@12897
   404
val vimage_def = thm "vimage_def";
wenzelm@12897
   405
val vimage_empty = thm "vimage_empty";
wenzelm@12897
   406
val vimage_eq = thm "vimage_eq";
wenzelm@12897
   407
val vimage_eq_UN = thm "vimage_eq_UN";
wenzelm@12897
   408
val vimage_insert = thm "vimage_insert";
wenzelm@12897
   409
val vimage_mono = thm "vimage_mono";
wenzelm@12897
   410
val vimage_singleton_eq = thm "vimage_singleton_eq";
wenzelm@12897
   411
wenzelm@11979
   412
structure Set =
wenzelm@11979
   413
struct
wenzelm@11979
   414
  val thy = the_context ();
wenzelm@11979
   415
  val Ball_def = Ball_def;
wenzelm@11979
   416
  val Bex_def = Bex_def;
wenzelm@11979
   417
  val Collect_mem_eq = Collect_mem_eq;
wenzelm@11979
   418
  val Compl_def = Compl_def;
wenzelm@11979
   419
  val INTER_def = INTER_def;
wenzelm@11979
   420
  val Int_def = Int_def;
wenzelm@11979
   421
  val Inter_def = Inter_def;
wenzelm@11979
   422
  val Pow_def = Pow_def;
wenzelm@11979
   423
  val UNION_def = UNION_def;
wenzelm@11979
   424
  val UNIV_def = UNIV_def;
wenzelm@11979
   425
  val Un_def = Un_def;
wenzelm@11979
   426
  val Union_def = Union_def;
wenzelm@11979
   427
  val empty_def = empty_def;
wenzelm@11979
   428
  val image_def = image_def;
wenzelm@11979
   429
  val insert_def = insert_def;
wenzelm@11979
   430
  val mem_Collect_eq = mem_Collect_eq;
wenzelm@11979
   431
  val psubset_def = psubset_def;
wenzelm@11979
   432
  val set_diff_def = set_diff_def;
wenzelm@11979
   433
  val subset_def = subset_def;
wenzelm@11979
   434
end;