src/HOL/Relation.ML
changeset 21669 c68717c16013
parent 21668 2d811ae6752a
child 21670 704510b508ef
     1.1 --- a/src/HOL/Relation.ML	Tue Dec 05 22:14:53 2006 +0100
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,100 +0,0 @@
     1.4 -
     1.5 -(* legacy ML bindings *)
     1.6 -
     1.7 -val DomainE = thm "DomainE";
     1.8 -val DomainI = thm "DomainI";
     1.9 -val Domain_Collect_split = thm "Domain_Collect_split";
    1.10 -val Domain_Diff_subset = thm "Domain_Diff_subset";
    1.11 -val Domain_Id = thm "Domain_Id";
    1.12 -val Domain_Int_subset = thm "Domain_Int_subset";
    1.13 -val Domain_Un_eq = thm "Domain_Un_eq";
    1.14 -val Domain_Union = thm "Domain_Union";
    1.15 -val Domain_def = thm "Domain_def";
    1.16 -val Domain_diag = thm "Domain_diag";
    1.17 -val Domain_empty = thm "Domain_empty";
    1.18 -val Domain_iff = thm "Domain_iff";
    1.19 -val Domain_insert = thm "Domain_insert";
    1.20 -val Domain_mono = thm "Domain_mono";
    1.21 -val Field_def = thm "Field_def";
    1.22 -val IdE = thm "IdE";
    1.23 -val IdI = thm "IdI";
    1.24 -val Id_O_R = thm "Id_O_R";
    1.25 -val Id_def = thm "Id_def";
    1.26 -val ImageE = thm "ImageE";
    1.27 -val ImageI = thm "ImageI";
    1.28 -val Image_Collect_split = thm "Image_Collect_split";
    1.29 -val Image_INT_subset = thm "Image_INT_subset";
    1.30 -val Image_Id = thm "Image_Id";
    1.31 -val Image_Int_subset = thm "Image_Int_subset";
    1.32 -val Image_UN = thm "Image_UN";
    1.33 -val Image_Un = thm "Image_Un";
    1.34 -val Image_def = thm "Image_def";
    1.35 -val Image_diag = thm "Image_diag";
    1.36 -val Image_empty = thm "Image_empty";
    1.37 -val Image_eq_UN = thm "Image_eq_UN";
    1.38 -val Image_iff = thm "Image_iff";
    1.39 -val Image_mono = thm "Image_mono";
    1.40 -val Image_singleton = thm "Image_singleton";
    1.41 -val Image_singleton_iff = thm "Image_singleton_iff";
    1.42 -val Image_subset = thm "Image_subset";
    1.43 -val Image_subset_eq = thm "Image_subset_eq";
    1.44 -val O_assoc = thm "O_assoc";
    1.45 -val R_O_Id = thm "R_O_Id";
    1.46 -val RangeE = thm "RangeE";
    1.47 -val RangeI = thm "RangeI";
    1.48 -val Range_Collect_split = thm "Range_Collect_split";
    1.49 -val Range_Diff_subset = thm "Range_Diff_subset";
    1.50 -val Range_Id = thm "Range_Id";
    1.51 -val Range_Int_subset = thm "Range_Int_subset";
    1.52 -val Range_Un_eq = thm "Range_Un_eq";
    1.53 -val Range_Union = thm "Range_Union";
    1.54 -val Range_def = thm "Range_def";
    1.55 -val Range_diag = thm "Range_diag";
    1.56 -val Range_empty = thm "Range_empty";
    1.57 -val Range_iff = thm "Range_iff";
    1.58 -val Range_insert = thm "Range_insert";
    1.59 -val antisymD = thm "antisymD";
    1.60 -val antisymI = thm "antisymI";
    1.61 -val antisym_Id = thm "antisym_Id";
    1.62 -val antisym_converse = thm "antisym_converse";
    1.63 -val antisym_def = thm "antisym_def";
    1.64 -val converseD = thm "converseD";
    1.65 -val converseE = thm "converseE";
    1.66 -val converseI = thm "converseI";
    1.67 -val converse_Id = thm "converse_Id";
    1.68 -val converse_converse = thm "converse_converse";
    1.69 -val converse_def = thm "converse_def";
    1.70 -val converse_diag = thm "converse_diag";
    1.71 -val converse_iff = thm "converse_iff";
    1.72 -val converse_rel_comp = thm "converse_rel_comp";
    1.73 -val diagE = thm "diagE";
    1.74 -val diagI = thm "diagI";
    1.75 -val diag_def = thm "diag_def";
    1.76 -val diag_eqI = thm "diag_eqI";
    1.77 -val diag_iff = thm "diag_iff";
    1.78 -val diag_subset_Times = thm "diag_subset_Times";
    1.79 -val inv_image_def = thm "inv_image_def";
    1.80 -val pair_in_Id_conv = thm "pair_in_Id_conv";
    1.81 -val reflD = thm "reflD";
    1.82 -val reflI = thm "reflI";
    1.83 -val refl_converse = thm "refl_converse";
    1.84 -val refl_def = thm "refl_def";
    1.85 -val reflexive_Id = thm "reflexive_Id";
    1.86 -val rel_compE = thm "rel_compE";
    1.87 -val rel_compEpair = thm "rel_compEpair";
    1.88 -val rel_compI = thm "rel_compI";
    1.89 -val rel_comp_def = thm "rel_comp_def";
    1.90 -val rel_comp_mono = thm "rel_comp_mono";
    1.91 -val rel_comp_subset_Sigma = thm "rel_comp_subset_Sigma";
    1.92 -val rev_ImageI = thm "rev_ImageI";
    1.93 -val single_valuedD = thm "single_valuedD";
    1.94 -val single_valuedI = thm "single_valuedI";
    1.95 -val single_valued_def = thm "single_valued_def";
    1.96 -val sym_def = thm "sym_def";
    1.97 -val transD = thm "transD";
    1.98 -val transI = thm "transI";
    1.99 -val trans_Id = thm "trans_Id";
   1.100 -val trans_O_subset = thm "trans_O_subset";
   1.101 -val trans_converse = thm "trans_converse";
   1.102 -val trans_def = thm "trans_def";
   1.103 -val trans_inv_image = thm "trans_inv_image";