| changeset 42018 | 878f33040280 |
| parent 41589 | bbd861837ebc |
| child 42770 | 3ebce8d71a05 |
--- a/src/HOL/TLA/Memory/MemoryImplementation.thy Sun Mar 20 22:48:08 2011 +0100 +++ b/src/HOL/TLA/Memory/MemoryImplementation.thy Sun Mar 20 23:07:06 2011 +0100 @@ -10,8 +10,7 @@ datatype histState = histA | histB -types - histType = "(PrIds => histState) stfun" (* the type of the history variable *) +type_synonym histType = "(PrIds => histState) stfun" (* the type of the history variable *) consts (* the specification *)