--- a/src/HOL/Factorial.thy Sun Sep 23 21:49:31 2018 +0200
+++ b/src/HOL/Factorial.thy Mon Sep 24 14:30:09 2018 +0200
@@ -403,13 +403,13 @@
subsection \<open>Misc\<close>
lemma fact_code [code]:
- "fact n = (of_nat (fold_atLeastAtMost_nat (( * )) 2 n 1) :: 'a::semiring_char_0)"
+ "fact n = (of_nat (fold_atLeastAtMost_nat ((*)) 2 n 1) :: 'a::semiring_char_0)"
proof -
have "fact n = (of_nat (\<Prod>{1..n}) :: 'a)"
by (simp add: fact_prod)
also have "\<Prod>{1..n} = \<Prod>{2..n}"
by (intro prod.mono_neutral_right) auto
- also have "\<dots> = fold_atLeastAtMost_nat (( * )) 2 n 1"
+ also have "\<dots> = fold_atLeastAtMost_nat ((*)) 2 n 1"
by (simp add: prod_atLeastAtMost_code)
finally show ?thesis .
qed