src/HOL/Import/HOL/option.imp
author haftmann
Mon Jan 30 08:20:56 2006 +0100 (2006-01-30)
changeset 18851 9502ce541f01
parent 14516 a183dec876ab
child 44763 b50d5d694838
permissions -rw-r--r--
adaptions to codegen_package
skalberg@14516
     1
import
skalberg@14516
     2
skalberg@14516
     3
import_segment "hol4"
skalberg@14516
     4
skalberg@14516
     5
type_maps
skalberg@14516
     6
  "option" > "Datatype.option"
skalberg@14516
     7
skalberg@14516
     8
const_maps
skalberg@14516
     9
  "option_case" > "Datatype.option.option_case"
skalberg@14516
    10
  "THE" > "Datatype.the"
skalberg@14516
    11
  "SOME" > "Datatype.option.Some"
skalberg@14516
    12
  "OPTION_MAP" > "Datatype.option_map"
skalberg@14516
    13
  "OPTION_JOIN" > "HOL4Compat.OPTION_JOIN"
skalberg@14516
    14
  "NONE" > "Datatype.option.None"
skalberg@14516
    15
  "IS_SOME" > "HOL4Compat.IS_SOME"
skalberg@14516
    16
  "IS_NONE" > "HOL4Compat.IS_NONE"
skalberg@14516
    17
skalberg@14516
    18
thm_maps
skalberg@14516
    19
  "option_nchotomy" > "Datatype.option.nchotomy"
skalberg@14516
    20
  "option_induction" > "HOL4Compat.OPTION_JOIN.induct"
skalberg@14516
    21
  "option_case_def" > "HOL4Compat.option_case_def"
skalberg@14516
    22
  "option_case_cong" > "HOL4Base.option.option_case_cong"
skalberg@14516
    23
  "option_case_compute" > "HOL4Base.option.option_case_compute"
skalberg@14516
    24
  "option_CLAUSES" > "HOL4Base.option.option_CLAUSES"
skalberg@14516
    25
  "THE_DEF" > "Datatype.the.simps"
skalberg@14516
    26
  "SOME_11" > "Datatype.option.simps_3"
skalberg@14516
    27
  "OPTION_MAP_EQ_SOME" > "HOL4Base.option.OPTION_MAP_EQ_SOME"
skalberg@14516
    28
  "OPTION_MAP_EQ_NONE" > "Datatype.option_map_is_None"
skalberg@14516
    29
  "OPTION_MAP_DEF" > "HOL4Compat.OPTION_MAP_DEF"
skalberg@14516
    30
  "OPTION_JOIN_EQ_SOME" > "HOL4Base.option.OPTION_JOIN_EQ_SOME"
skalberg@14516
    31
  "OPTION_JOIN_DEF" > "HOL4Compat.OPTION_JOIN_DEF"
skalberg@14516
    32
  "NOT_SOME_NONE" > "Datatype.option.simps_2"
skalberg@14516
    33
  "NOT_NONE_SOME" > "Datatype.option.simps_1"
skalberg@14516
    34
  "IS_SOME_DEF" > "HOL4Compat.IS_SOME_DEF"
skalberg@14516
    35
  "IS_NONE_DEF" > "HOL4Compat.IS_NONE_DEF"
skalberg@14516
    36
skalberg@14516
    37
ignore_thms
skalberg@14516
    38
  "option_axiom"
skalberg@14516
    39
  "option_TY_DEF"
skalberg@14516
    40
  "option_REP_ABS_DEF"
skalberg@14516
    41
  "option_Axiom"
skalberg@14516
    42
  "SOME_DEF"
skalberg@14516
    43
  "NONE_DEF"
skalberg@14516
    44
skalberg@14516
    45
end