src/HOL/Import/HOL/marker.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 def_maps
     6   "stmarker" > "stmarker_primdef"
     7 
     8 const_maps
     9   "stmarker" > "HOL4Base.marker.stmarker"
    10 
    11 thm_maps
    12   "stmarker_primdef" > "HOL4Base.marker.stmarker_primdef"
    13   "stmarker_def" > "HOL4Base.marker.stmarker_def"
    14   "move_right_disj" > "HOL4Base.marker.move_right_disj"
    15   "move_right_conj" > "HOL4Base.marker.move_right_conj"
    16   "move_left_disj" > "HOL4Base.marker.move_left_disj"
    17   "move_left_conj" > "HOL4Base.marker.move_left_conj"
    18 
    19 end