changeset 69064 | 5840724b1d71 |
parent 68660 | 4ce18f389f53 |
child 69597 | ff784d5a5bfb |
--- a/src/HOL/Quotient_Examples/Quotient_Int.thy Sun Sep 23 21:49:31 2018 +0200 +++ b/src/HOL/Quotient_Examples/Quotient_Int.thy Mon Sep 24 14:30:09 2018 +0200 @@ -78,7 +78,7 @@ done quotient_definition - "(( * )) :: (int \<Rightarrow> int \<Rightarrow> int)" is "times_int_raw" + "((*)) :: (int \<Rightarrow> int \<Rightarrow> int)" is "times_int_raw" apply(rule equivp_transp[OF int_equivp]) apply(rule times_int_raw_fst) apply(assumption)