# HG changeset patch # User haftmann # Date 1267177700 -3600 # Node ID cb06a11a7955176c16e8409449092149f591d21e # Parent af1c8c15340e237b24fec114ffdb023dc1990cc2 implement quotient_of for odl SML code generator diff -r af1c8c15340e -r cb06a11a7955 src/HOL/Rat.thy --- a/src/HOL/Rat.thy Fri Feb 26 09:20:18 2010 +0100 +++ b/src/HOL/Rat.thy Fri Feb 26 10:48:20 2010 +0100 @@ -1168,6 +1168,9 @@ Fract ("(_,/ _)") consts_code + quotient_of ("{*normalize*}") + +consts_code "of_int :: int \ rat" ("\rat'_of'_int") attach {* fun rat_of_int i = (i, 1);