src/HOL/Import/HOL/res_quan.imp
author haftmann
Mon Jan 30 08:20:56 2006 +0100 (2006-01-30)
changeset 18851 9502ce541f01
parent 14516 a183dec876ab
permissions -rw-r--r--
adaptions to codegen_package
     1 import
     2 
     3 import_segment "hol4"
     4 
     5 thm_maps
     6   "RES_SELECT_UNIV" > "HOL4Vec.res_quan.RES_SELECT_UNIV"
     7   "RES_SELECT_EMPTY" > "HOL4Vec.res_quan.RES_SELECT_EMPTY"
     8   "RES_SELECT" > "HOL4Base.bool.RES_SELECT_DEF"
     9   "RES_FORALL_UNIV" > "HOL4Vec.res_quan.RES_FORALL_UNIV"
    10   "RES_FORALL_UNIQUE" > "HOL4Vec.res_quan.RES_FORALL_UNIQUE"
    11   "RES_FORALL_REORDER" > "HOL4Vec.res_quan.RES_FORALL_REORDER"
    12   "RES_FORALL_NULL" > "HOL4Vec.res_quan.RES_FORALL_NULL"
    13   "RES_FORALL_FORALL" > "HOL4Vec.res_quan.RES_FORALL_FORALL"
    14   "RES_FORALL_EMPTY" > "HOL4Vec.res_quan.RES_FORALL_EMPTY"
    15   "RES_FORALL_DISJ_DIST" > "HOL4Vec.res_quan.RES_FORALL_DISJ_DIST"
    16   "RES_FORALL_CONJ_DIST" > "HOL4Vec.res_quan.RES_FORALL_CONJ_DIST"
    17   "RES_FORALL" > "HOL4Base.bool.RES_FORALL_DEF"
    18   "RES_EXISTS_UNIV" > "HOL4Vec.res_quan.RES_EXISTS_UNIV"
    19   "RES_EXISTS_UNIQUE_UNIV" > "HOL4Vec.res_quan.RES_EXISTS_UNIQUE_UNIV"
    20   "RES_EXISTS_UNIQUE_NULL" > "HOL4Vec.res_quan.RES_EXISTS_UNIQUE_NULL"
    21   "RES_EXISTS_UNIQUE_EMPTY" > "HOL4Vec.res_quan.RES_EXISTS_UNIQUE_EMPTY"
    22   "RES_EXISTS_UNIQUE_ALT" > "HOL4Vec.res_quan.RES_EXISTS_UNIQUE_ALT"
    23   "RES_EXISTS_UNIQUE" > "HOL4Base.bool.RES_EXISTS_UNIQUE_DEF"
    24   "RES_EXISTS_REORDER" > "HOL4Vec.res_quan.RES_EXISTS_REORDER"
    25   "RES_EXISTS_NULL" > "HOL4Vec.res_quan.RES_EXISTS_NULL"
    26   "RES_EXISTS_EQUAL" > "HOL4Vec.res_quan.RES_EXISTS_EQUAL"
    27   "RES_EXISTS_EMPTY" > "HOL4Vec.res_quan.RES_EXISTS_EMPTY"
    28   "RES_EXISTS_DISJ_DIST" > "HOL4Vec.res_quan.RES_EXISTS_DISJ_DIST"
    29   "RES_EXISTS_ALT" > "HOL4Vec.res_quan.RES_EXISTS_ALT"
    30   "RES_EXISTS" > "HOL4Base.bool.RES_EXISTS_DEF"
    31   "RES_DISJ_EXISTS_DIST" > "HOL4Vec.res_quan.RES_DISJ_EXISTS_DIST"
    32   "RES_ABSTRACT_IDEMPOT" > "HOL4Vec.res_quan.RES_ABSTRACT_IDEMPOT"
    33   "RES_ABSTRACT_EQUAL_EQ" > "HOL4Vec.res_quan.RES_ABSTRACT_EQUAL_EQ"
    34   "RES_ABSTRACT_EQUAL" > "HOL4Vec.res_quan.RES_ABSTRACT_EQUAL"
    35   "RES_ABSTRACT" > "HOL4Vec.res_quan.RES_ABSTRACT"
    36 
    37 end