equal
deleted
inserted
replaced
106 |
106 |
107 definition |
107 definition |
108 SIGN :: "my_int \<Rightarrow> my_int" |
108 SIGN :: "my_int \<Rightarrow> my_int" |
109 where |
109 where |
110 "SIGN i = (if i = ZERO then ZERO else if (LESS ZERO i) then ONE else (NEG ONE))" |
110 "SIGN i = (if i = ZERO then ZERO else if (LESS ZERO i) then ONE else (NEG ONE))" |
|
111 |
|
112 ML {* print_qconstinfo @{context} *} |
|
113 |
|
114 ML {* print_qconstinfo @{context} *} |
111 |
115 |
112 lemma plus_sym_pre: |
116 lemma plus_sym_pre: |
113 shows "my_plus a b \<approx> my_plus b a" |
117 shows "my_plus a b \<approx> my_plus b a" |
114 apply(cases a) |
118 apply(cases a) |
115 apply(cases b) |
119 apply(cases b) |