| changeset 37678 | 0040bafffdef |
| parent 35354 | 2e8dc3c64430 |
| child 42018 | 878f33040280 |
--- a/src/HOL/TLA/Action.thy Thu Jul 01 16:54:42 2010 +0200 +++ b/src/HOL/TLA/Action.thy Thu Jul 01 16:54:44 2010 +0200 @@ -16,8 +16,7 @@ 'a trfun = "(state * state) => 'a" action = "bool trfun" -arities - "*" :: (world, world) world +arities prod :: (world, world) world consts (** abstract syntax **)