equal
deleted
inserted
replaced
2379 have "k \<noteq> 0 \<Longrightarrow> l \<noteq> 0 \<Longrightarrow> 0 < l \<and> 0 \<le> k \<or> l < 0 \<and> k < 0 \<longleftrightarrow> sgn k = sgn l" |
2379 have "k \<noteq> 0 \<Longrightarrow> l \<noteq> 0 \<Longrightarrow> 0 < l \<and> 0 \<le> k \<or> l < 0 \<and> k < 0 \<longleftrightarrow> sgn k = sgn l" |
2380 by (auto simp add: not_less sgn_if) |
2380 by (auto simp add: not_less sgn_if) |
2381 then show ?thesis by (simp add: divmod_int_pdivmod) |
2381 then show ?thesis by (simp add: divmod_int_pdivmod) |
2382 qed |
2382 qed |
2383 |
2383 |
2384 code_modulename SML |
2384 code_identifier |
2385 Divides Arith |
2385 code_module Divides \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith |
2386 |
|
2387 code_modulename OCaml |
|
2388 Divides Arith |
|
2389 |
|
2390 code_modulename Haskell |
|
2391 Divides Arith |
|
2392 |
2386 |
2393 end |
2387 end |
|
2388 |