equal
deleted
inserted
replaced
127 |
127 |
128 lemma "(i::int) mod 42 <= 41" |
128 lemma "(i::int) mod 42 <= 41" |
129 (* FIXME: arith does not know about iszero *) |
129 (* FIXME: arith does not know about iszero *) |
130 apply (tactic {* lin_arith_pre_tac @{context} 1 *}) |
130 apply (tactic {* lin_arith_pre_tac @{context} 1 *}) |
131 oops |
131 oops |
|
132 |
|
133 lemma "-(i::int) * 1 = 0 ==> i = 0" |
|
134 by (tactic {* fast_arith_tac @{context} 1 *}) |
|
135 |
|
136 lemma "[| (0::int) < abs i; abs i * 1 < abs i * j |] ==> 1 < abs i * j" |
|
137 by (tactic {* fast_arith_tac @{context} 1 *}) |
132 |
138 |
133 |
139 |
134 subsection {* Meta-Logic *} |
140 subsection {* Meta-Logic *} |
135 |
141 |
136 lemma "x < Suc y == x <= y" |
142 lemma "x < Suc y == x <= y" |