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 (<)"