src/HOL/TLA/Stfun.thy
changeset 42018 878f33040280
parent 35354 2e8dc3c64430
child 55382 9218fa411c15
     1.1 --- a/src/HOL/TLA/Stfun.thy	Sun Mar 20 22:48:08 2011 +0100
     1.2 +++ b/src/HOL/TLA/Stfun.thy	Sun Mar 20 23:07:06 2011 +0100
     1.3 @@ -13,9 +13,8 @@
     1.4  
     1.5  arities state :: world
     1.6  
     1.7 -types
     1.8 -  'a stfun = "state => 'a"
     1.9 -  stpred  = "bool stfun"
    1.10 +type_synonym 'a stfun = "state => 'a"
    1.11 +type_synonym stpred  = "bool stfun"
    1.12  
    1.13  
    1.14  consts