changeset 60429 | d3d1e185cd63 |
parent 58889 | 5b7a9633cfa8 |
child 61076 | bdc1e2f0a86a |
--- a/src/HOL/Import/HOL_Light_Maps.thy Thu Jun 11 21:41:55 2015 +0100 +++ b/src/HOL/Import/HOL_Light_Maps.thy Fri Jun 12 08:53:23 2015 +0200 @@ -198,7 +198,7 @@ by simp import_const_map MOD : mod -import_const_map DIV : div +import_const_map DIV : divide lemma DIVISION_0: "\<forall>m n\<Colon>nat. if n = id 0 then m div n = id 0 \<and> m mod n = m else m = m div n * n + m mod n \<and> m mod n < n"