src/HOL/Import/HOL/bool.imp
author Cezary Kaliszyk <kaliszyk@in.tum.de>
Wed, 07 Sep 2011 07:59:45 +0900
changeset 44763 b50d5d694838
parent 39302 d7728f65b353
permissions -rw-r--r--
HOL/Import: Update HOL4 generated files to current Isabelle.
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
44763
b50d5d694838 HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 39302
diff changeset
    14
type_maps
b50d5d694838 HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 39302
diff changeset
    15
  "bool" > "HOL.bool"
b50d5d694838 HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 39302
diff changeset
    16
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    17
const_maps
38556
dc92eee56ed7 deglobalized named HOL constants
haftmann
parents: 17916
diff changeset
    18
  "~" > "HOL.Not"
44763
b50d5d694838 HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 39302
diff changeset
    19
  "bool_case" > "Product_Type.bool.bool_case"
b50d5d694838 HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 39302
diff changeset
    20
  "\\/" > "HOL.disj"
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    21
  "TYPE_DEFINITION" > "HOL4Setup.TYPE_DEFINITION"
38556
dc92eee56ed7 deglobalized named HOL constants
haftmann
parents: 17916
diff changeset
    22
  "T" > "HOL.True"
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    23
  "RES_SELECT" > "HOL4Base.bool.RES_SELECT"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    24
  "RES_FORALL" > "HOL4Base.bool.RES_FORALL"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    25
  "RES_EXISTS_UNIQUE" > "HOL4Base.bool.RES_EXISTS_UNIQUE"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    26
  "RES_EXISTS" > "HOL4Base.bool.RES_EXISTS"
17644
bd59bfd4bf37 fixed disambiguation problem
obua
parents: 17268
diff changeset
    27
  "ONTO" > "Fun.surj"
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    28
  "ONE_ONE" > "HOL4Setup.ONE_ONE"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    29
  "LET" > "HOL4Compat.LET"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    30
  "IN" > "HOL4Base.bool.IN"
38556
dc92eee56ed7 deglobalized named HOL constants
haftmann
parents: 17916
diff changeset
    31
  "F" > "HOL.False"
16587
b34c8aa657a5 Constant "If" is now local
paulson
parents: 15647
diff changeset
    32
  "COND" > "HOL.If"
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    33
  "ARB" > "HOL4Base.bool.ARB"
38556
dc92eee56ed7 deglobalized named HOL constants
haftmann
parents: 17916
diff changeset
    34
  "?!" > "HOL.Ex1"
dc92eee56ed7 deglobalized named HOL constants
haftmann
parents: 17916
diff changeset
    35
  "?" > "HOL.Ex"
44763
b50d5d694838 HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 39302
diff changeset
    36
  "/\\" > "HOL.conj"
38556
dc92eee56ed7 deglobalized named HOL constants
haftmann
parents: 17916
diff changeset
    37
  "!" > "HOL.All"
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    38
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    39
thm_maps
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    40
  "bool_case_thm" > "HOL4Base.bool.bool_case_thm"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    41
  "bool_case_ID" > "HOL4Base.bool.bool_case_ID"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    42
  "bool_case_DEF" > "HOL4Compat.bool_case_DEF"
44763
b50d5d694838 HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 39302
diff changeset
    43
  "bool_INDUCT" > "Product_Type.bool.induct"
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    44
  "boolAxiom" > "HOL4Base.bool.boolAxiom"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    45
  "UNWIND_THM2" > "HOL.simp_thms_39"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    46
  "UNWIND_THM1" > "HOL.simp_thms_40"
17652
b1ef33ebfa17 Release HOL4 and HOLLight Importer.
obua
parents: 17644
diff changeset
    47
  "UNWIND_FORALL_THM2" > "HOL.simp_thms_41"
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    48
  "UNWIND_FORALL_THM1" > "HOL.simp_thms_42"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    49
  "UEXISTS_SIMP" > "HOL4Base.bool.UEXISTS_SIMP"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    50
  "UEXISTS_OR_THM" > "HOL4Base.bool.UEXISTS_OR_THM"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    51
  "T_DEF" > "HOL.True_def"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    52
  "TYPE_DEFINITION_THM" > "HOL4Setup.TYPE_DEFINITION"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    53
  "TYPE_DEFINITION" > "HOL4Setup.TYPE_DEFINITION"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    54
  "TRUTH" > "HOL.TrueI"
44763
b50d5d694838 HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 39302
diff changeset
    55
  "SWAP_FORALL_THM" > "HOL.all_comm"
b50d5d694838 HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 39302
diff changeset
    56
  "SWAP_EXISTS_THM" > "HOL.ex_comm"
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    57
  "SKOLEM_THM" > "HOL4Base.bool.SKOLEM_THM"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    58
  "SELECT_UNIQUE" > "HOL4Base.bool.SELECT_UNIQUE"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    59
  "SELECT_THM" > "HOL4Setup.EXISTS_DEF"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    60
  "SELECT_REFL_2" > "Hilbert_Choice.some_sym_eq_trivial"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    61
  "SELECT_REFL" > "Hilbert_Choice.some_eq_trivial"
44763
b50d5d694838 HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 39302
diff changeset
    62
  "SELECT_AX" > "Hilbert_Choice.someI"
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    63
  "RIGHT_OR_OVER_AND" > "HOL.disj_conj_distribR"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    64
  "RIGHT_OR_EXISTS_THM" > "HOL.ex_simps_4"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    65
  "RIGHT_FORALL_OR_THM" > "HOL.all_simps_4"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    66
  "RIGHT_FORALL_IMP_THM" > "HOL.all_simps_6"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    67
  "RIGHT_EXISTS_IMP_THM" > "HOL.ex_simps_6"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    68
  "RIGHT_EXISTS_AND_THM" > "HOL.ex_simps_2"
44763
b50d5d694838 HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 39302
diff changeset
    69
  "RIGHT_AND_OVER_OR" > "Groebner_Basis.dnf_2"
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    70
  "RIGHT_AND_FORALL_THM" > "HOL.all_simps_2"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    71
  "RES_SELECT_def" > "HOL4Base.bool.RES_SELECT_def"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    72
  "RES_SELECT_DEF" > "HOL4Base.bool.RES_SELECT_DEF"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    73
  "RES_FORALL_def" > "HOL4Base.bool.RES_FORALL_def"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    74
  "RES_FORALL_DEF" > "HOL4Base.bool.RES_FORALL_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_EXISTS_UNIQUE_def" > "HOL4Base.bool.RES_EXISTS_UNIQUE_def"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    77
  "RES_EXISTS_UNIQUE_DEF" > "HOL4Base.bool.RES_EXISTS_UNIQUE_DEF"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    78
  "RES_EXISTS_DEF" > "HOL4Base.bool.RES_EXISTS_DEF"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    79
  "RES_ABSTRACT_DEF" > "HOL4Base.bool.RES_ABSTRACT_DEF"
44763
b50d5d694838 HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 39302
diff changeset
    80
  "REFL_CLAUSE" > "Groebner_Basis.bool_simps_6"
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    81
  "OR_INTRO_THM2" > "HOL.disjI2"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    82
  "OR_INTRO_THM1" > "HOL.disjI1"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    83
  "OR_IMP_THM" > "HOL4Base.bool.OR_IMP_THM"
44763
b50d5d694838 HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 39302
diff changeset
    84
  "OR_ELIM_THM" > "HOL.disjE"
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    85
  "OR_DEF" > "HOL.or_def"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    86
  "OR_CONG" > "HOL4Base.bool.OR_CONG"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    87
  "OR_CLAUSES" > "HOL4Base.bool.OR_CLAUSES"
17644
bd59bfd4bf37 fixed disambiguation problem
obua
parents: 17268
diff changeset
    88
  "ONTO_THM" > "Fun.surj_def"
bd59bfd4bf37 fixed disambiguation problem
obua
parents: 17268
diff changeset
    89
  "ONTO_DEF" > "Fun.surj_def"
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    90
  "ONE_ONE_THM" > "HOL4Base.bool.ONE_ONE_THM"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    91
  "ONE_ONE_DEF" > "HOL4Setup.ONE_ONE_DEF"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    92
  "NOT_IMP" > "HOL.not_imp"
44763
b50d5d694838 HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 39302
diff changeset
    93
  "NOT_FORALL_THM" > "HOL.not_all"
b50d5d694838 HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 39302
diff changeset
    94
  "NOT_F" > "Groebner_Basis.PFalse_2"
b50d5d694838 HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 39302
diff changeset
    95
  "NOT_EXISTS_THM" > "HOL.not_ex"
b50d5d694838 HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 39302
diff changeset
    96
  "NOT_DEF" > "Groebner_Basis.bool_simps_19"
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    97
  "NOT_CLAUSES" > "HOL4Base.bool.NOT_CLAUSES"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    98
  "NOT_AND" > "HOL4Base.bool.NOT_AND"
17188
a26a4fc323ed Updated import.
obua
parents: 16587
diff changeset
    99
  "MONO_OR" > "Inductive.basic_monos_3"
44763
b50d5d694838 HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 39302
diff changeset
   100
  "MONO_NOT" > "HOL.contrapos_nn"
17652
b1ef33ebfa17 Release HOL4 and HOLLight Importer.
obua
parents: 17644
diff changeset
   101
  "MONO_IMP" > "Set.imp_mono"
17188
a26a4fc323ed Updated import.
obua
parents: 16587
diff changeset
   102
  "MONO_EXISTS" > "Inductive.basic_monos_5"
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   103
  "MONO_COND" > "HOL4Base.bool.MONO_COND"
17188
a26a4fc323ed Updated import.
obua
parents: 16587
diff changeset
   104
  "MONO_AND" > "Inductive.basic_monos_4"
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   105
  "MONO_ALL" > "Inductive.basic_monos_6"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   106
  "LET_THM" > "HOL.Let_def"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   107
  "LET_RATOR" > "HOL4Base.bool.LET_RATOR"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   108
  "LET_RAND" > "HOL4Base.bool.LET_RAND"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   109
  "LET_DEF" > "HOL4Compat.LET_def"
44763
b50d5d694838 HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 39302
diff changeset
   110
  "LET_CONG" > "FunDef.let_cong"
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   111
  "LEFT_OR_OVER_AND" > "HOL.disj_conj_distribL"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   112
  "LEFT_OR_EXISTS_THM" > "HOL.ex_simps_3"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   113
  "LEFT_FORALL_OR_THM" > "HOL.all_simps_3"
44763
b50d5d694838 HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 39302
diff changeset
   114
  "LEFT_FORALL_IMP_THM" > "HOL.all_simps_5"
b50d5d694838 HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 39302
diff changeset
   115
  "LEFT_EXISTS_IMP_THM" > "HOL.ex_simps_5"
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   116
  "LEFT_EXISTS_AND_THM" > "HOL.ex_simps_1"
44763
b50d5d694838 HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 39302
diff changeset
   117
  "LEFT_AND_OVER_OR" > "Groebner_Basis.dnf_1"
17652
b1ef33ebfa17 Release HOL4 and HOLLight Importer.
obua
parents: 17644
diff changeset
   118
  "LEFT_AND_FORALL_THM" > "HOL.all_simps_1"
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   119
  "IN_def" > "HOL4Base.bool.IN_def"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   120
  "IN_DEF" > "HOL4Base.bool.IN_DEF"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   121
  "INFINITY_AX" > "HOL4Setup.INFINITY_AX"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   122
  "IMP_F_EQ_F" > "HOL4Base.bool.IMP_F_EQ_F"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   123
  "IMP_F" > "HOL.notI"
44763
b50d5d694838 HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 39302
diff changeset
   124
  "IMP_DISJ_THM" > "Groebner_Basis.nnf_simps_3"
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   125
  "IMP_CONG" > "HOL.imp_cong"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   126
  "IMP_CLAUSES" > "HOL4Base.bool.IMP_CLAUSES"
44763
b50d5d694838 HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 39302
diff changeset
   127
  "IMP_ANTISYM_AX" > "HOL.iff"
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   128
  "F_IMP" > "HOL4Base.bool.F_IMP"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   129
  "F_DEF" > "HOL.False_def"
44763
b50d5d694838 HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 39302
diff changeset
   130
  "FUN_EQ_THM" > "HOL.fun_eq_iff"
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   131
  "FORALL_THM" > "HOL4Base.bool.FORALL_THM"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   132
  "FORALL_SIMP" > "HOL.simp_thms_35"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   133
  "FORALL_DEF" > "HOL.All_def"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   134
  "FORALL_AND_THM" > "HOL.all_conj_distrib"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   135
  "FALSITY" > "HOL.FalseE"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   136
  "EXISTS_UNIQUE_THM" > "HOL4Compat.EXISTS_UNIQUE_DEF"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   137
  "EXISTS_UNIQUE_REFL" > "HOL.ex1_eq_1"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   138
  "EXISTS_UNIQUE_DEF" > "HOL4Compat.EXISTS_UNIQUE_DEF"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   139
  "EXISTS_THM" > "HOL4Base.bool.EXISTS_THM"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   140
  "EXISTS_SIMP" > "HOL.simp_thms_36"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   141
  "EXISTS_REFL" > "HOL.simp_thms_37"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   142
  "EXISTS_OR_THM" > "HOL.ex_disj_distrib"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   143
  "EXISTS_DEF" > "HOL4Setup.EXISTS_DEF"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   144
  "EXCLUDED_MIDDLE" > "HOL4Base.bool.EXCLUDED_MIDDLE"
44763
b50d5d694838 HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 39302
diff changeset
   145
  "ETA_THM" > "HOL.eta_contract_eq"
b50d5d694838 HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 39302
diff changeset
   146
  "ETA_AX" > "HOL.eta_contract_eq"
b50d5d694838 HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 39302
diff changeset
   147
  "EQ_TRANS" > "HOL.trans"
b50d5d694838 HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 39302
diff changeset
   148
  "EQ_SYM_EQ" > "HOL.eq_ac_1"
b50d5d694838 HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 39302
diff changeset
   149
  "EQ_SYM" > "HOL.eq_reflection"
b50d5d694838 HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 39302
diff changeset
   150
  "EQ_REFL" > "HOL.refl"
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   151
  "EQ_IMP_THM" > "HOL.iff_conv_conj_imp"
44763
b50d5d694838 HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 39302
diff changeset
   152
  "EQ_EXT" > "HOL.eq_reflection"
b50d5d694838 HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 39302
diff changeset
   153
  "EQ_EXPAND" > "Groebner_Basis.nnf_simps_4"
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   154
  "EQ_CLAUSES" > "HOL4Base.bool.EQ_CLAUSES"
44763
b50d5d694838 HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 39302
diff changeset
   155
  "DISJ_SYM" > "Groebner_Basis.dnf_4"
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   156
  "DISJ_IMP_THM" > "HOL.imp_disjL"
44763
b50d5d694838 HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 39302
diff changeset
   157
  "DISJ_COMM" > "Groebner_Basis.dnf_4"
b50d5d694838 HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 39302
diff changeset
   158
  "DISJ_ASSOC" > "HOL.disj_ac_3"
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   159
  "DE_MORGAN_THM" > "HOL4Base.bool.DE_MORGAN_THM"
44763
b50d5d694838 HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 39302
diff changeset
   160
  "CONJ_SYM" > "Groebner_Basis.dnf_3"
b50d5d694838 HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 39302
diff changeset
   161
  "CONJ_COMM" > "Groebner_Basis.dnf_3"
b50d5d694838 HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 39302
diff changeset
   162
  "CONJ_ASSOC" > "HOL.conj_ac_3"
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   163
  "COND_RATOR" > "HOL4Base.bool.COND_RATOR"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   164
  "COND_RAND" > "HOL.if_distrib"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   165
  "COND_ID" > "HOL.if_cancel"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   166
  "COND_EXPAND" > "HOL4Base.bool.COND_EXPAND"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   167
  "COND_DEF" > "HOL4Compat.COND_DEF"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   168
  "COND_CONG" > "HOL4Base.bool.COND_CONG"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   169
  "COND_CLAUSES" > "HOL4Base.bool.COND_CLAUSES"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   170
  "COND_ABS" > "HOL4Base.bool.COND_ABS"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   171
  "BOTH_FORALL_OR_THM" > "HOL4Base.bool.BOTH_FORALL_OR_THM"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   172
  "BOTH_FORALL_IMP_THM" > "HOL4Base.bool.BOTH_FORALL_IMP_THM"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   173
  "BOTH_EXISTS_IMP_THM" > "HOL4Base.bool.BOTH_EXISTS_IMP_THM"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   174
  "BOTH_EXISTS_AND_THM" > "HOL4Base.bool.BOTH_EXISTS_AND_THM"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   175
  "BOOL_FUN_INDUCT" > "HOL4Base.bool.BOOL_FUN_INDUCT"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   176
  "BOOL_FUN_CASES_THM" > "HOL4Base.bool.BOOL_FUN_CASES_THM"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   177
  "BOOL_EQ_DISTINCT" > "HOL4Base.bool.BOOL_EQ_DISTINCT"
44763
b50d5d694838 HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 39302
diff changeset
   178
  "BOOL_CASES_AX" > "HOL.True_or_False"
b50d5d694838 HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 39302
diff changeset
   179
  "BETA_THM" > "HOL.eta_contract_eq"
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   180
  "ARB_def" > "HOL4Base.bool.ARB_def"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   181
  "ARB_DEF" > "HOL4Base.bool.ARB_DEF"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   182
  "AND_INTRO_THM" > "HOL.conjI"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   183
  "AND_IMP_INTRO" > "HOL.imp_conjL"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   184
  "AND_DEF" > "HOL.and_def"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   185
  "AND_CONG" > "HOL4Base.bool.AND_CONG"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   186
  "AND_CLAUSES" > "HOL4Base.bool.AND_CLAUSES"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   187
  "AND2_THM" > "HOL.conjunct2"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   188
  "AND1_THM" > "HOL.conjunct1"
44763
b50d5d694838 HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 39302
diff changeset
   189
  "ABS_SIMP" > "HOL.refl"
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   190
  "ABS_REP_THM" > "HOL4Base.bool.ABS_REP_THM"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   191
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   192
ignore_thms
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   193
  "UNBOUNDED_THM"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   194
  "UNBOUNDED_DEF"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   195
  "BOUNDED_THM"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   196
  "BOUNDED_DEF"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   197
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   198
end