src/HOL/Import/HOL/bool.imp
author obua
Mon, 29 Aug 2005 16:51:39 +0200
changeset 17188 a26a4fc323ed
parent 16587 b34c8aa657a5
child 17268 309288714d9d
permissions -rw-r--r--
Updated import.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
     1
import
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
     2
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
     3
import_segment "hol4"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
     4
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
     5
def_maps
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
     6
  "RES_SELECT" > "RES_SELECT_def"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
     7
  "RES_FORALL" > "RES_FORALL_def"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
     8
  "RES_EXISTS_UNIQUE" > "RES_EXISTS_UNIQUE_def"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
     9
  "RES_EXISTS" > "RES_EXISTS_def"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    10
  "RES_ABSTRACT" > "RES_ABSTRACT_def"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    11
  "IN" > "IN_def"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    12
  "ARB" > "ARB_def"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    13
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    14
const_maps
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    15
  "~" > "Not"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    16
  "bool_case" > "Datatype.bool.bool_case"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    17
  "\\/" > "op |"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    18
  "TYPE_DEFINITION" > "HOL4Setup.TYPE_DEFINITION"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    19
  "T" > "True"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    20
  "RES_SELECT" > "HOL4Base.bool.RES_SELECT"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    21
  "RES_FORALL" > "HOL4Base.bool.RES_FORALL"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    22
  "RES_EXISTS_UNIQUE" > "HOL4Base.bool.RES_EXISTS_UNIQUE"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    23
  "RES_EXISTS" > "HOL4Base.bool.RES_EXISTS"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    24
  "ONTO" > "HOL4Setup.ONTO"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    25
  "ONE_ONE" > "HOL4Setup.ONE_ONE"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    26
  "LET" > "HOL4Compat.LET"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    27
  "IN" > "HOL4Base.bool.IN"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    28
  "F" > "False"
16587
b34c8aa657a5 Constant "If" is now local
paulson
parents: 15647
diff changeset
    29
  "COND" > "HOL.If"
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    30
  "ARB" > "HOL4Base.bool.ARB"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    31
  "?!" > "Ex1"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    32
  "?" > "Ex"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    33
  "/\\" > "op &"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    34
  "!" > "All"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    35
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    36
thm_maps
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    37
  "bool_case_thm" > "HOL4Base.bool.bool_case_thm"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    38
  "bool_case_ID" > "HOL4Base.bool.bool_case_ID"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    39
  "bool_case_DEF" > "HOL4Compat.bool_case_DEF"
15647
b1f486a9c56b Updated import configuration.
skalberg
parents: 14516
diff changeset
    40
  "bool_INDUCT" > "Datatype.bool.induct"
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    41
  "boolAxiom" > "HOL4Base.bool.boolAxiom"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    42
  "UNWIND_THM2" > "HOL.simp_thms_39"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    43
  "UNWIND_THM1" > "HOL.simp_thms_40"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    44
  "UNWIND_FORALL_THM2" > "HOL.simp_thms_41"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    45
  "UNWIND_FORALL_THM1" > "HOL.simp_thms_42"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    46
  "UEXISTS_SIMP" > "HOL4Base.bool.UEXISTS_SIMP"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    47
  "UEXISTS_OR_THM" > "HOL4Base.bool.UEXISTS_OR_THM"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    48
  "T_DEF" > "HOL.True_def"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    49
  "TYPE_DEFINITION_THM" > "HOL4Setup.TYPE_DEFINITION"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    50
  "TYPE_DEFINITION" > "HOL4Setup.TYPE_DEFINITION"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    51
  "TRUTH" > "HOL.TrueI"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    52
  "SWAP_FORALL_THM" > "HOL4Base.bool.SWAP_FORALL_THM"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    53
  "SWAP_EXISTS_THM" > "HOL4Base.bool.SWAP_EXISTS_THM"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    54
  "SKOLEM_THM" > "HOL4Base.bool.SKOLEM_THM"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    55
  "SELECT_UNIQUE" > "HOL4Base.bool.SELECT_UNIQUE"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    56
  "SELECT_THM" > "HOL4Setup.EXISTS_DEF"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    57
  "SELECT_REFL_2" > "Hilbert_Choice.some_sym_eq_trivial"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    58
  "SELECT_REFL" > "Hilbert_Choice.some_eq_trivial"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    59
  "SELECT_AX" > "Hilbert_Choice.tfl_some"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    60
  "RIGHT_OR_OVER_AND" > "HOL.disj_conj_distribR"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    61
  "RIGHT_OR_EXISTS_THM" > "HOL.ex_simps_4"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    62
  "RIGHT_FORALL_OR_THM" > "HOL.all_simps_4"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    63
  "RIGHT_FORALL_IMP_THM" > "HOL.all_simps_6"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    64
  "RIGHT_EXISTS_IMP_THM" > "HOL.ex_simps_6"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    65
  "RIGHT_EXISTS_AND_THM" > "HOL.ex_simps_2"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    66
  "RIGHT_AND_OVER_OR" > "HOL.conj_disj_distribR"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    67
  "RIGHT_AND_FORALL_THM" > "HOL.all_simps_2"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    68
  "RES_SELECT_def" > "HOL4Base.bool.RES_SELECT_def"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    69
  "RES_SELECT_DEF" > "HOL4Base.bool.RES_SELECT_DEF"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    70
  "RES_FORALL_def" > "HOL4Base.bool.RES_FORALL_def"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    71
  "RES_FORALL_DEF" > "HOL4Base.bool.RES_FORALL_DEF"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    72
  "RES_EXISTS_def" > "HOL4Base.bool.RES_EXISTS_def"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    73
  "RES_EXISTS_UNIQUE_def" > "HOL4Base.bool.RES_EXISTS_UNIQUE_def"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    74
  "RES_EXISTS_UNIQUE_DEF" > "HOL4Base.bool.RES_EXISTS_UNIQUE_DEF"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    75
  "RES_EXISTS_DEF" > "HOL4Base.bool.RES_EXISTS_DEF"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    76
  "RES_ABSTRACT_DEF" > "HOL4Base.bool.RES_ABSTRACT_DEF"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    77
  "REFL_CLAUSE" > "HOL.simp_thms_6"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    78
  "OR_INTRO_THM2" > "HOL.disjI2"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    79
  "OR_INTRO_THM1" > "HOL.disjI1"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    80
  "OR_IMP_THM" > "HOL4Base.bool.OR_IMP_THM"
17188
a26a4fc323ed Updated import.
obua
parents: 16587
diff changeset
    81
  "OR_ELIM_THM" > "Recdef.tfl_disjE"
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    82
  "OR_DEF" > "HOL.or_def"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    83
  "OR_CONG" > "HOL4Base.bool.OR_CONG"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    84
  "OR_CLAUSES" > "HOL4Base.bool.OR_CLAUSES"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    85
  "ONTO_THM" > "HOL4Setup.ONTO_DEF"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    86
  "ONTO_DEF" > "HOL4Setup.ONTO_DEF"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    87
  "ONE_ONE_THM" > "HOL4Base.bool.ONE_ONE_THM"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    88
  "ONE_ONE_DEF" > "HOL4Setup.ONE_ONE_DEF"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    89
  "NOT_IMP" > "HOL.not_imp"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    90
  "NOT_FORALL_THM" > "Inductive.basic_monos_15"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    91
  "NOT_F" > "HOL.Eq_FalseI"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    92
  "NOT_EXISTS_THM" > "Inductive.basic_monos_16"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    93
  "NOT_DEF" > "HOL.simp_thms_19"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    94
  "NOT_CLAUSES" > "HOL4Base.bool.NOT_CLAUSES"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    95
  "NOT_AND" > "HOL4Base.bool.NOT_AND"
17188
a26a4fc323ed Updated import.
obua
parents: 16587
diff changeset
    96
  "MONO_OR" > "Inductive.basic_monos_3"
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    97
  "MONO_NOT" > "HOL.rev_contrapos"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    98
  "MONO_IMP" > "Set.imp_mono"
17188
a26a4fc323ed Updated import.
obua
parents: 16587
diff changeset
    99
  "MONO_EXISTS" > "Inductive.basic_monos_5"
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   100
  "MONO_COND" > "HOL4Base.bool.MONO_COND"
17188
a26a4fc323ed Updated import.
obua
parents: 16587
diff changeset
   101
  "MONO_AND" > "Inductive.basic_monos_4"
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   102
  "MONO_ALL" > "Inductive.basic_monos_6"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   103
  "LET_THM" > "HOL.Let_def"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   104
  "LET_RATOR" > "HOL4Base.bool.LET_RATOR"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   105
  "LET_RAND" > "HOL4Base.bool.LET_RAND"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   106
  "LET_DEF" > "HOL4Compat.LET_def"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   107
  "LET_CONG" > "Recdef.let_cong"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   108
  "LEFT_OR_OVER_AND" > "HOL.disj_conj_distribL"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   109
  "LEFT_OR_EXISTS_THM" > "HOL.ex_simps_3"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   110
  "LEFT_FORALL_OR_THM" > "HOL.all_simps_3"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   111
  "LEFT_FORALL_IMP_THM" > "HOL.imp_ex"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   112
  "LEFT_EXISTS_IMP_THM" > "HOL.imp_all"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   113
  "LEFT_EXISTS_AND_THM" > "HOL.ex_simps_1"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   114
  "LEFT_AND_OVER_OR" > "HOL.conj_disj_distribL"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   115
  "LEFT_AND_FORALL_THM" > "HOL.all_simps_1"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   116
  "IN_def" > "HOL4Base.bool.IN_def"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   117
  "IN_DEF" > "HOL4Base.bool.IN_DEF"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   118
  "INFINITY_AX" > "HOL4Setup.INFINITY_AX"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   119
  "IMP_F_EQ_F" > "HOL4Base.bool.IMP_F_EQ_F"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   120
  "IMP_F" > "HOL.notI"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   121
  "IMP_DISJ_THM" > "Inductive.basic_monos_11"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   122
  "IMP_CONG" > "HOL.imp_cong"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   123
  "IMP_CLAUSES" > "HOL4Base.bool.IMP_CLAUSES"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   124
  "IMP_ANTISYM_AX" > "HOL4Setup.light_imp_as"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   125
  "F_IMP" > "HOL4Base.bool.F_IMP"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   126
  "F_DEF" > "HOL.False_def"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   127
  "FUN_EQ_THM" > "Fun.expand_fun_eq"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   128
  "FORALL_THM" > "HOL4Base.bool.FORALL_THM"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   129
  "FORALL_SIMP" > "HOL.simp_thms_35"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   130
  "FORALL_DEF" > "HOL.All_def"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   131
  "FORALL_AND_THM" > "HOL.all_conj_distrib"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   132
  "FALSITY" > "HOL.FalseE"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   133
  "EXISTS_UNIQUE_THM" > "HOL4Compat.EXISTS_UNIQUE_DEF"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   134
  "EXISTS_UNIQUE_REFL" > "HOL.ex1_eq_1"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   135
  "EXISTS_UNIQUE_DEF" > "HOL4Compat.EXISTS_UNIQUE_DEF"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   136
  "EXISTS_THM" > "HOL4Base.bool.EXISTS_THM"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   137
  "EXISTS_SIMP" > "HOL.simp_thms_36"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   138
  "EXISTS_REFL" > "HOL.simp_thms_37"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   139
  "EXISTS_OR_THM" > "HOL.ex_disj_distrib"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   140
  "EXISTS_DEF" > "HOL4Setup.EXISTS_DEF"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   141
  "EXCLUDED_MIDDLE" > "HOL4Base.bool.EXCLUDED_MIDDLE"
17188
a26a4fc323ed Updated import.
obua
parents: 16587
diff changeset
   142
  "ETA_THM" > "Presburger.fm_modd_pinf"
a26a4fc323ed Updated import.
obua
parents: 16587
diff changeset
   143
  "ETA_AX" > "Presburger.fm_modd_pinf"
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   144
  "EQ_TRANS" > "Set.basic_trans_rules_31"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   145
  "EQ_SYM_EQ" > "HOL.eq_sym_conv"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   146
  "EQ_SYM" > "HOL.meta_eq_to_obj_eq"
17188
a26a4fc323ed Updated import.
obua
parents: 16587
diff changeset
   147
  "EQ_REFL" > "Presburger.fm_modd_pinf"
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   148
  "EQ_IMP_THM" > "HOL.iff_conv_conj_imp"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   149
  "EQ_EXT" > "HOL.meta_eq_to_obj_eq"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   150
  "EQ_EXPAND" > "HOL4Base.bool.EQ_EXPAND"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   151
  "EQ_CLAUSES" > "HOL4Base.bool.EQ_CLAUSES"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   152
  "DISJ_SYM" > "HOL.disj_comms_1"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   153
  "DISJ_IMP_THM" > "HOL.imp_disjL"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   154
  "DISJ_COMM" > "HOL.disj_comms_1"
17188
a26a4fc323ed Updated import.
obua
parents: 16587
diff changeset
   155
  "DISJ_ASSOC" > "Recdef.tfl_disj_assoc"
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   156
  "DE_MORGAN_THM" > "HOL4Base.bool.DE_MORGAN_THM"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   157
  "CONJ_SYM" > "HOL.conj_comms_1"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   158
  "CONJ_COMM" > "HOL.conj_comms_1"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   159
  "CONJ_ASSOC" > "HOL.conj_assoc"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   160
  "COND_RATOR" > "HOL4Base.bool.COND_RATOR"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   161
  "COND_RAND" > "HOL.if_distrib"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   162
  "COND_ID" > "HOL.if_cancel"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   163
  "COND_EXPAND" > "HOL4Base.bool.COND_EXPAND"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   164
  "COND_DEF" > "HOL4Compat.COND_DEF"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   165
  "COND_CONG" > "HOL4Base.bool.COND_CONG"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   166
  "COND_CLAUSES" > "HOL4Base.bool.COND_CLAUSES"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   167
  "COND_ABS" > "HOL4Base.bool.COND_ABS"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   168
  "BOTH_FORALL_OR_THM" > "HOL4Base.bool.BOTH_FORALL_OR_THM"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   169
  "BOTH_FORALL_IMP_THM" > "HOL4Base.bool.BOTH_FORALL_IMP_THM"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   170
  "BOTH_EXISTS_IMP_THM" > "HOL4Base.bool.BOTH_EXISTS_IMP_THM"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   171
  "BOTH_EXISTS_AND_THM" > "HOL4Base.bool.BOTH_EXISTS_AND_THM"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   172
  "BOOL_FUN_INDUCT" > "HOL4Base.bool.BOOL_FUN_INDUCT"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   173
  "BOOL_FUN_CASES_THM" > "HOL4Base.bool.BOOL_FUN_CASES_THM"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   174
  "BOOL_EQ_DISTINCT" > "HOL4Base.bool.BOOL_EQ_DISTINCT"
15647
b1f486a9c56b Updated import configuration.
skalberg
parents: 14516
diff changeset
   175
  "BOOL_CASES_AX" > "Datatype.bool.nchotomy"
17188
a26a4fc323ed Updated import.
obua
parents: 16587
diff changeset
   176
  "BETA_THM" > "Presburger.fm_modd_pinf"
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   177
  "ARB_def" > "HOL4Base.bool.ARB_def"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   178
  "ARB_DEF" > "HOL4Base.bool.ARB_DEF"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   179
  "AND_INTRO_THM" > "HOL.conjI"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   180
  "AND_IMP_INTRO" > "HOL.imp_conjL"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   181
  "AND_DEF" > "HOL.and_def"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   182
  "AND_CONG" > "HOL4Base.bool.AND_CONG"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   183
  "AND_CLAUSES" > "HOL4Base.bool.AND_CLAUSES"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   184
  "AND2_THM" > "HOL.conjunct2"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   185
  "AND1_THM" > "HOL.conjunct1"
17188
a26a4fc323ed Updated import.
obua
parents: 16587
diff changeset
   186
  "ABS_SIMP" > "Presburger.fm_modd_pinf"
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   187
  "ABS_REP_THM" > "HOL4Base.bool.ABS_REP_THM"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   188
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   189
ignore_thms
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   190
  "UNBOUNDED_THM"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   191
  "UNBOUNDED_DEF"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   192
  "BOUNDED_THM"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   193
  "BOUNDED_DEF"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   194
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   195
end