src/HOL/GCD.thy
changeset 69906 55534affe445
parent 69785 9e326f6f8a24
     1.1 --- a/src/HOL/GCD.thy	Sun Mar 10 15:16:45 2019 +0000
     1.2 +++ b/src/HOL/GCD.thy	Sun Mar 10 15:16:45 2019 +0000
     1.3 @@ -2735,7 +2735,7 @@
     1.4  
     1.5  code_printing
     1.6    constant "gcd :: integer \<Rightarrow> _" \<rightharpoonup>
     1.7 -    (OCaml) "Big'_int.gcd'_big'_int"
     1.8 +    (OCaml) "!(fun k l -> if Z.equal k Z.zero then/ Z.abs l else if Z.equal/ l Z.zero then Z.abs k else Z.gcd k l)"
     1.9    and (Haskell) "Prelude.gcd"
    1.10    and (Scala) "_.gcd'((_)')"
    1.11    \<comment> \<open>There is no gcd operation in the SML standard library, so no code setup for SML\<close>