# 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 \<Rightarrow> rat" ("\<module>rat'_of'_int")
 attach {*
 fun rat_of_int i = (i, 1);