src/HOL/Import/HOL_Light_Maps.thy

 
 lemma FACT[import_const "FACT" : fact]:
   "fact (id 0) = id (bit1 0) \<and> (\<forall>n. fact (Suc n) = Suc n * fact n)"
   by simp
 
-import_const_map MOD : mod
+import_const_map MOD : modulo
 import_const_map DIV : divide
 
 lemma DIVISION_0:
   "\<forall>m n::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"
   by simp