src/HOL/Import/HOL/one.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 type_maps
     6   "one" > "Product_Type.unit"
     7 
     8 const_maps
     9   "one" > "Product_Type.Unity"
    10 
    11 thm_maps
    12   "one" > "HOL4Compat.one"
    13 
    14 ignore_thms
    15   "one_axiom"
    16   "one_TY_DEF"
    17   "one_DEF"
    18   "one_Axiom"
    19 
    20 end