equal
deleted
inserted
replaced
98 definition |
98 definition |
99 SIGN :: "my_int \<Rightarrow> my_int" |
99 SIGN :: "my_int \<Rightarrow> my_int" |
100 where |
100 where |
101 "SIGN i = (if i = ZERO then ZERO else if (LESS ZERO i) then ONE else (NEG ONE))" |
101 "SIGN i = (if i = ZERO then ZERO else if (LESS ZERO i) then ONE else (NEG ONE))" |
102 |
102 |
103 ML {* print_qconstinfo @{context} *} |
103 ML {* Quotient_Info.print_qconstinfo @{context} *} |
104 |
104 |
105 lemma plus_sym_pre: |
105 lemma plus_sym_pre: |
106 shows "my_plus a b \<approx> my_plus b a" |
106 shows "my_plus a b \<approx> my_plus b a" |
107 apply(cases a) |
107 apply(cases a) |
108 apply(cases b) |
108 apply(cases b) |