src/HOL/Relation.ML
author nipkow
Wed Aug 18 11:09:40 2004 +0200 (2004-08-18)
changeset 15140 322485b816ac
parent 13639 8ee6ea6627e1
permissions -rw-r--r--
import -> imports
     1 
     2 (* legacy ML bindings *)
     3 
     4 val DomainE = thm "DomainE";
     5 val DomainI = thm "DomainI";
     6 val Domain_Collect_split = thm "Domain_Collect_split";
     7 val Domain_Diff_subset = thm "Domain_Diff_subset";
     8 val Domain_Id = thm "Domain_Id";
     9 val Domain_Int_subset = thm "Domain_Int_subset";
    10 val Domain_Un_eq = thm "Domain_Un_eq";
    11 val Domain_Union = thm "Domain_Union";
    12 val Domain_def = thm "Domain_def";
    13 val Domain_diag = thm "Domain_diag";
    14 val Domain_empty = thm "Domain_empty";
    15 val Domain_iff = thm "Domain_iff";
    16 val Domain_insert = thm "Domain_insert";
    17 val Domain_mono = thm "Domain_mono";
    18 val Field_def = thm "Field_def";
    19 val IdE = thm "IdE";
    20 val IdI = thm "IdI";
    21 val Id_O_R = thm "Id_O_R";
    22 val Id_def = thm "Id_def";
    23 val ImageE = thm "ImageE";
    24 val ImageI = thm "ImageI";
    25 val Image_Collect_split = thm "Image_Collect_split";
    26 val Image_INT_subset = thm "Image_INT_subset";
    27 val Image_Id = thm "Image_Id";
    28 val Image_Int_subset = thm "Image_Int_subset";
    29 val Image_UN = thm "Image_UN";
    30 val Image_Un = thm "Image_Un";
    31 val Image_def = thm "Image_def";
    32 val Image_diag = thm "Image_diag";
    33 val Image_empty = thm "Image_empty";
    34 val Image_eq_UN = thm "Image_eq_UN";
    35 val Image_iff = thm "Image_iff";
    36 val Image_mono = thm "Image_mono";
    37 val Image_singleton = thm "Image_singleton";
    38 val Image_singleton_iff = thm "Image_singleton_iff";
    39 val Image_subset = thm "Image_subset";
    40 val Image_subset_eq = thm "Image_subset_eq";
    41 val O_assoc = thm "O_assoc";
    42 val R_O_Id = thm "R_O_Id";
    43 val RangeE = thm "RangeE";
    44 val RangeI = thm "RangeI";
    45 val Range_Collect_split = thm "Range_Collect_split";
    46 val Range_Diff_subset = thm "Range_Diff_subset";
    47 val Range_Id = thm "Range_Id";
    48 val Range_Int_subset = thm "Range_Int_subset";
    49 val Range_Un_eq = thm "Range_Un_eq";
    50 val Range_Union = thm "Range_Union";
    51 val Range_def = thm "Range_def";
    52 val Range_diag = thm "Range_diag";
    53 val Range_empty = thm "Range_empty";
    54 val Range_iff = thm "Range_iff";
    55 val Range_insert = thm "Range_insert";
    56 val antisymD = thm "antisymD";
    57 val antisymI = thm "antisymI";
    58 val antisym_Id = thm "antisym_Id";
    59 val antisym_converse = thm "antisym_converse";
    60 val antisym_def = thm "antisym_def";
    61 val converseD = thm "converseD";
    62 val converseE = thm "converseE";
    63 val converseI = thm "converseI";
    64 val converse_Id = thm "converse_Id";
    65 val converse_converse = thm "converse_converse";
    66 val converse_def = thm "converse_def";
    67 val converse_diag = thm "converse_diag";
    68 val converse_iff = thm "converse_iff";
    69 val converse_rel_comp = thm "converse_rel_comp";
    70 val diagE = thm "diagE";
    71 val diagI = thm "diagI";
    72 val diag_def = thm "diag_def";
    73 val diag_eqI = thm "diag_eqI";
    74 val diag_iff = thm "diag_iff";
    75 val diag_subset_Times = thm "diag_subset_Times";
    76 val inv_image_def = thm "inv_image_def";
    77 val pair_in_Id_conv = thm "pair_in_Id_conv";
    78 val reflD = thm "reflD";
    79 val reflI = thm "reflI";
    80 val refl_converse = thm "refl_converse";
    81 val refl_def = thm "refl_def";
    82 val reflexive_Id = thm "reflexive_Id";
    83 val rel_compE = thm "rel_compE";
    84 val rel_compEpair = thm "rel_compEpair";
    85 val rel_compI = thm "rel_compI";
    86 val rel_comp_def = thm "rel_comp_def";
    87 val rel_comp_mono = thm "rel_comp_mono";
    88 val rel_comp_subset_Sigma = thm "rel_comp_subset_Sigma";
    89 val rev_ImageI = thm "rev_ImageI";
    90 val single_valuedD = thm "single_valuedD";
    91 val single_valuedI = thm "single_valuedI";
    92 val single_valued_def = thm "single_valued_def";
    93 val sym_def = thm "sym_def";
    94 val transD = thm "transD";
    95 val transI = thm "transI";
    96 val trans_Id = thm "trans_Id";
    97 val trans_O_subset = thm "trans_O_subset";
    98 val trans_converse = thm "trans_converse";
    99 val trans_def = thm "trans_def";
   100 val trans_inv_image = thm "trans_inv_image";