src/HOL/TLA/Intensional.thy
changeset 69064 5840724b1d71
parent 67399 eab6ce8368fa
child 69597 ff784d5a5bfb
--- a/src/HOL/TLA/Intensional.thy	Sun Sep 23 21:49:31 2018 +0200
+++ b/src/HOL/TLA/Intensional.thy	Mon Sep 24 14:30:09 2018 +0200
@@ -119,7 +119,7 @@
   "_liftIf"       == "_lift3 (CONST If)"
   "_liftPlus"     == "_lift2 (+)"
   "_liftMinus"    == "_lift2 (-)"
-  "_liftTimes"    == "_lift2 (( * ))"
+  "_liftTimes"    == "_lift2 ((*))"
   "_liftDiv"      == "_lift2 (div)"
   "_liftMod"      == "_lift2 (mod)"
   "_liftLess"     == "_lift2 (<)"