src/HOL/Import/HOL_Light_Maps.thy
changeset 60429 d3d1e185cd63
parent 58889 5b7a9633cfa8
child 61076 bdc1e2f0a86a
     1.1 --- a/src/HOL/Import/HOL_Light_Maps.thy	Thu Jun 11 21:41:55 2015 +0100
     1.2 +++ b/src/HOL/Import/HOL_Light_Maps.thy	Fri Jun 12 08:53:23 2015 +0200
     1.3 @@ -198,7 +198,7 @@
     1.4    by simp
     1.5  
     1.6  import_const_map MOD : mod
     1.7 -import_const_map DIV : div
     1.8 +import_const_map DIV : divide
     1.9  
    1.10  lemma DIVISION_0:
    1.11    "\<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"