src/HOL/Library/Executable_Rat.thy
changeset 24223 fa9421d52c74
parent 24197 c9e3cb5e5681
equal deleted inserted replaced
24222:a8a28c15c5cc 24223:fa9421d52c74
    92 
    92 
    93 lemma rat_div_code [code]: "Rat x / Rat y = Rat (x \<div>\<^sub>N y)"
    93 lemma rat_div_code [code]: "Rat x / Rat y = Rat (x \<div>\<^sub>N y)"
    94   unfolding Rat_def by simp
    94   unfolding Rat_def by simp
    95 
    95 
    96 code_modulename SML
    96 code_modulename SML
       
    97   Rational Rational
    97   Executable_Rat Rational
    98   Executable_Rat Rational
    98 
    99 
    99 code_modulename OCaml
   100 code_modulename OCaml
       
   101   Rational Rational
   100   Executable_Rat Rational
   102   Executable_Rat Rational
   101 
   103 
   102 code_modulename Haskell
   104 code_modulename Haskell
       
   105   Rational Rational
   103   Executable_Rat Rational
   106   Executable_Rat Rational
   104 
   107 
   105 end
   108 end