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
     1 import
     2 
     3 import_segment "hol4"
     4 
     5 type_maps
     6   "option" > "Datatype.option"
     7 
     8 const_maps
     9   "option_case" > "Datatype.option.option_case"
    10   "THE" > "Datatype.the"
    11   "SOME" > "Datatype.option.Some"
    12   "OPTION_MAP" > "Datatype.option_map"
    13   "OPTION_JOIN" > "HOL4Compat.OPTION_JOIN"
    14   "NONE" > "Datatype.option.None"
    15   "IS_SOME" > "HOL4Compat.IS_SOME"
    16   "IS_NONE" > "HOL4Compat.IS_NONE"
    17 
    18 thm_maps
    19   "option_nchotomy" > "Datatype.option.nchotomy"
    20   "option_induction" > "HOL4Compat.OPTION_JOIN.induct"
    21   "option_case_def" > "HOL4Compat.option_case_def"
    22   "option_case_cong" > "HOL4Base.option.option_case_cong"
    23   "option_case_compute" > "HOL4Base.option.option_case_compute"
    24   "option_CLAUSES" > "HOL4Base.option.option_CLAUSES"
    25   "THE_DEF" > "Datatype.the.simps"
    26   "SOME_11" > "Datatype.option.simps_3"
    27   "OPTION_MAP_EQ_SOME" > "HOL4Base.option.OPTION_MAP_EQ_SOME"
    28   "OPTION_MAP_EQ_NONE" > "Datatype.option_map_is_None"
    29   "OPTION_MAP_DEF" > "HOL4Compat.OPTION_MAP_DEF"
    30   "OPTION_JOIN_EQ_SOME" > "HOL4Base.option.OPTION_JOIN_EQ_SOME"
    31   "OPTION_JOIN_DEF" > "HOL4Compat.OPTION_JOIN_DEF"
    32   "NOT_SOME_NONE" > "Datatype.option.simps_2"
    33   "NOT_NONE_SOME" > "Datatype.option.simps_1"
    34   "IS_SOME_DEF" > "HOL4Compat.IS_SOME_DEF"
    35   "IS_NONE_DEF" > "HOL4Compat.IS_NONE_DEF"
    36 
    37 ignore_thms
    38   "option_axiom"
    39   "option_TY_DEF"
    40   "option_REP_ABS_DEF"
    41   "option_Axiom"
    42   "SOME_DEF"
    43   "NONE_DEF"
    44 
    45 end