| changeset 31672 | 2f8e3150e073 |
| parent 31666 | 760c612ad800 |
| child 31674 | d0115c303846 |
| 31671:81e5e8ffe92f | 31672:2f8e3150e073 |
|---|---|
1058 Fract ("(_,/ _)") |
1058 Fract ("(_,/ _)") |
1059 |
1059 |
1060 consts_code |
1060 consts_code |
1061 "of_int :: int \<Rightarrow> rat" ("\<module>rat'_of'_int") |
1061 "of_int :: int \<Rightarrow> rat" ("\<module>rat'_of'_int") |
1062 attach {* |
1062 attach {* |
1063 fun rat_of_int i (i, 1); |
1063 fun = rat_of_int i (i, 1); |
1064 *} |
1064 *} |
1065 |
1065 |
1066 end |
1066 end |