src/HOL/Num.thy
changeset 52435 6646bb548c6b
parent 52210 0226035df99d
child 53064 7e3f39bc41df
equal deleted inserted replaced
52434:cbb94074682b 52435:6646bb548c6b
  1112 hide_const (open) One Bit0 Bit1 BitM inc pow sqr sub dbl dbl_inc dbl_dec
  1112 hide_const (open) One Bit0 Bit1 BitM inc pow sqr sub dbl dbl_inc dbl_dec
  1113 
  1113 
  1114 
  1114 
  1115 subsection {* code module namespace *}
  1115 subsection {* code module namespace *}
  1116 
  1116 
  1117 code_modulename SML
  1117 code_identifier
  1118   Num Arith
  1118   code_module Num \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
  1119 
  1119 
  1120 code_modulename OCaml
  1120 end
  1121   Num Arith
  1121 
  1122 
  1122 
  1123 code_modulename Haskell
       
  1124   Num Arith
       
  1125 
       
  1126 end
       
  1127 
       
  1128