src/HOL/Import/HOL/prob_pseudo.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   "pseudo_linear_tl" > "pseudo_linear_tl_primdef"
     7   "pseudo_linear_hd" > "pseudo_linear_hd_primdef"
     8   "pseudo_linear1" > "pseudo_linear1_primdef"
     9   "pseudo" > "pseudo_primdef"
    10 
    11 const_maps
    12   "pseudo_linear_tl" > "HOL4Prob.prob_pseudo.pseudo_linear_tl"
    13   "pseudo_linear_hd" > "HOL4Prob.prob_pseudo.pseudo_linear_hd"
    14   "pseudo" > "HOL4Prob.prob_pseudo.pseudo"
    15 
    16 thm_maps
    17   "pseudo_primdef" > "HOL4Prob.prob_pseudo.pseudo_primdef"
    18   "pseudo_linear_tl_primdef" > "HOL4Prob.prob_pseudo.pseudo_linear_tl_primdef"
    19   "pseudo_linear_tl_def" > "HOL4Prob.prob_pseudo.pseudo_linear_tl_def"
    20   "pseudo_linear_hd_primdef" > "HOL4Prob.prob_pseudo.pseudo_linear_hd_primdef"
    21   "pseudo_linear_hd_def" > "HOL4Prob.prob_pseudo.pseudo_linear_hd_def"
    22   "pseudo_linear1_def" > "HOL4Prob.prob_pseudo.pseudo_linear1_def"
    23   "pseudo_def" > "HOL4Prob.prob_pseudo.pseudo_def"
    24   "PSEUDO_LINEAR1_EXECUTE" > "HOL4Prob.prob_pseudo.PSEUDO_LINEAR1_EXECUTE"
    25 
    26 end