equal
deleted
inserted
replaced
116 |
116 |
117 definition |
117 definition |
118 SIGN :: "my_int \<Rightarrow> my_int" |
118 SIGN :: "my_int \<Rightarrow> my_int" |
119 where |
119 where |
120 "SIGN i = (if i = ZERO then ZERO else if (LESS ZERO i) then ONE else (NEG ONE))" |
120 "SIGN i = (if i = ZERO then ZERO else if (LESS ZERO i) then ONE else (NEG ONE))" |
|
121 |
|
122 |
121 |
123 |
122 ML {* print_qconstinfo @{context} *} |
124 ML {* print_qconstinfo @{context} *} |
123 |
125 |
124 ML {* print_qconstinfo @{context} *} |
126 ML {* print_qconstinfo @{context} *} |
125 |
127 |