src/HOL/Import/HOL/sum.imp
author skalberg
Fri Apr 01 18:59:17 2005 +0200 (2005-04-01)
changeset 15647 b1f486a9c56b
parent 14516 a183dec876ab
child 44763 b50d5d694838
permissions -rw-r--r--
Updated import configuration.
skalberg@14516
     1
import
skalberg@14516
     2
skalberg@14516
     3
import_segment "hol4"
skalberg@14516
     4
skalberg@14516
     5
type_maps
skalberg@14516
     6
  "sum" > "+"
skalberg@14516
     7
skalberg@14516
     8
const_maps
skalberg@14516
     9
  "sum_case" > "Datatype.sum.sum_case"
skalberg@14516
    10
  "OUTR" > "HOL4Compat.OUTR"
skalberg@14516
    11
  "OUTL" > "HOL4Compat.OUTL"
skalberg@14516
    12
  "ISR" > "HOL4Compat.ISR"
skalberg@14516
    13
  "ISL" > "HOL4Compat.ISL"
skalberg@15647
    14
  "INR" > "Sum_Type.Inr"
skalberg@15647
    15
  "INL" > "Sum_Type.Inl"
skalberg@14516
    16
skalberg@14516
    17
thm_maps
skalberg@15647
    18
  "sum_distinct1" > "Datatype.sum.simps_2"
skalberg@15647
    19
  "sum_distinct" > "Datatype.sum.simps_1"
skalberg@14516
    20
  "sum_case_def" > "HOL4Compat.sum_case_def"
skalberg@14516
    21
  "sum_case_cong" > "HOL4Base.sum.sum_case_cong"
skalberg@14516
    22
  "sum_INDUCT" > "HOL4Compat.OUTR.induct"
skalberg@14516
    23
  "sum_CASES" > "Datatype.sum.nchotomy"
skalberg@14516
    24
  "OUTR" > "HOL4Compat.OUTR"
skalberg@14516
    25
  "OUTL" > "HOL4Compat.OUTL"
skalberg@14516
    26
  "ISR" > "HOL4Compat.ISR"
skalberg@14516
    27
  "ISL_OR_ISR" > "HOL4Base.sum.ISL_OR_ISR"
skalberg@14516
    28
  "ISL" > "HOL4Compat.ISL"
skalberg@15647
    29
  "INR_neq_INL" > "Datatype.sum.simps_2"
skalberg@14516
    30
  "INR_INL_11" > "HOL4Compat.INR_INL_11"
skalberg@14516
    31
  "INR" > "HOL4Base.sum.INR"
skalberg@14516
    32
  "INL" > "HOL4Base.sum.INL"
skalberg@14516
    33
skalberg@14516
    34
ignore_thms
skalberg@14516
    35
  "sum_axiom"
skalberg@14516
    36
  "sum_TY_DEF"
skalberg@14516
    37
  "sum_ISO_DEF"
skalberg@14516
    38
  "sum_Axiom"
skalberg@14516
    39
  "IS_SUM_REP"
skalberg@14516
    40
  "INR_DEF"
skalberg@14516
    41
  "INL_DEF"
skalberg@14516
    42
skalberg@14516
    43
end