changeset 42018 | 878f33040280 |
parent 41229 | d797baa3d57c |
child 42814 | 5af15f1e2ef6 |
--- a/src/HOL/TLA/Intensional.thy Sun Mar 20 22:48:08 2011 +0100 +++ b/src/HOL/TLA/Intensional.thy Sun Mar 20 23:07:06 2011 +0100 @@ -15,9 +15,8 @@ (** abstract syntax **) -types - ('w,'a) expr = "'w => 'a" (* intention: 'w::world, 'a::type *) - 'w form = "('w, bool) expr" +type_synonym ('w,'a) expr = "'w => 'a" (* intention: 'w::world, 'a::type *) +type_synonym 'w form = "('w, bool) expr" consts Valid :: "('w::world) form => bool"