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
skalberg@14516
     1
import
skalberg@14516
     2
skalberg@14516
     3
import_segment "hol4"
skalberg@14516
     4
skalberg@14516
     5
thm_maps
skalberg@14516
     6
  "RES_SELECT_UNIV" > "HOL4Vec.res_quan.RES_SELECT_UNIV"
skalberg@14516
     7
  "RES_SELECT_EMPTY" > "HOL4Vec.res_quan.RES_SELECT_EMPTY"
skalberg@14516
     8
  "RES_SELECT" > "HOL4Base.bool.RES_SELECT_DEF"
skalberg@14516
     9
  "RES_FORALL_UNIV" > "HOL4Vec.res_quan.RES_FORALL_UNIV"
skalberg@14516
    10
  "RES_FORALL_UNIQUE" > "HOL4Vec.res_quan.RES_FORALL_UNIQUE"
skalberg@14516
    11
  "RES_FORALL_REORDER" > "HOL4Vec.res_quan.RES_FORALL_REORDER"
skalberg@14516
    12
  "RES_FORALL_NULL" > "HOL4Vec.res_quan.RES_FORALL_NULL"
skalberg@14516
    13
  "RES_FORALL_FORALL" > "HOL4Vec.res_quan.RES_FORALL_FORALL"
skalberg@14516
    14
  "RES_FORALL_EMPTY" > "HOL4Vec.res_quan.RES_FORALL_EMPTY"
skalberg@14516
    15
  "RES_FORALL_DISJ_DIST" > "HOL4Vec.res_quan.RES_FORALL_DISJ_DIST"
skalberg@14516
    16
  "RES_FORALL_CONJ_DIST" > "HOL4Vec.res_quan.RES_FORALL_CONJ_DIST"
skalberg@14516
    17
  "RES_FORALL" > "HOL4Base.bool.RES_FORALL_DEF"
skalberg@14516
    18
  "RES_EXISTS_UNIV" > "HOL4Vec.res_quan.RES_EXISTS_UNIV"
skalberg@14516
    19
  "RES_EXISTS_UNIQUE_UNIV" > "HOL4Vec.res_quan.RES_EXISTS_UNIQUE_UNIV"
skalberg@14516
    20
  "RES_EXISTS_UNIQUE_NULL" > "HOL4Vec.res_quan.RES_EXISTS_UNIQUE_NULL"
skalberg@14516
    21
  "RES_EXISTS_UNIQUE_EMPTY" > "HOL4Vec.res_quan.RES_EXISTS_UNIQUE_EMPTY"
skalberg@14516
    22
  "RES_EXISTS_UNIQUE_ALT" > "HOL4Vec.res_quan.RES_EXISTS_UNIQUE_ALT"
skalberg@14516
    23
  "RES_EXISTS_UNIQUE" > "HOL4Base.bool.RES_EXISTS_UNIQUE_DEF"
skalberg@14516
    24
  "RES_EXISTS_REORDER" > "HOL4Vec.res_quan.RES_EXISTS_REORDER"
skalberg@14516
    25
  "RES_EXISTS_NULL" > "HOL4Vec.res_quan.RES_EXISTS_NULL"
skalberg@14516
    26
  "RES_EXISTS_EQUAL" > "HOL4Vec.res_quan.RES_EXISTS_EQUAL"
skalberg@14516
    27
  "RES_EXISTS_EMPTY" > "HOL4Vec.res_quan.RES_EXISTS_EMPTY"
skalberg@14516
    28
  "RES_EXISTS_DISJ_DIST" > "HOL4Vec.res_quan.RES_EXISTS_DISJ_DIST"
skalberg@14516
    29
  "RES_EXISTS_ALT" > "HOL4Vec.res_quan.RES_EXISTS_ALT"
skalberg@14516
    30
  "RES_EXISTS" > "HOL4Base.bool.RES_EXISTS_DEF"
skalberg@14516
    31
  "RES_DISJ_EXISTS_DIST" > "HOL4Vec.res_quan.RES_DISJ_EXISTS_DIST"
skalberg@14516
    32
  "RES_ABSTRACT_IDEMPOT" > "HOL4Vec.res_quan.RES_ABSTRACT_IDEMPOT"
skalberg@14516
    33
  "RES_ABSTRACT_EQUAL_EQ" > "HOL4Vec.res_quan.RES_ABSTRACT_EQUAL_EQ"
skalberg@14516
    34
  "RES_ABSTRACT_EQUAL" > "HOL4Vec.res_quan.RES_ABSTRACT_EQUAL"
skalberg@14516
    35
  "RES_ABSTRACT" > "HOL4Vec.res_quan.RES_ABSTRACT"
skalberg@14516
    36
skalberg@14516
    37
end