author | haftmann |
Fri, 26 Feb 2010 10:48:20 +0100 | |
changeset 35375 | cb06a11a7955 |
parent 35374 | af1c8c15340e |
child 35376 | 212b1dc5212d |
src/HOL/Rat.thy | file | annotate | diff | comparison | revisions |
--- 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);