implement quotient_of for odl SML code generator
authorhaftmann
Fri, 26 Feb 2010 10:48:20 +0100
changeset 35375 cb06a11a7955
parent 35374 af1c8c15340e
child 35376 212b1dc5212d
implement quotient_of for odl SML code generator
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);