modernized specifications;

--- a/src/HOL/TLA/Action.thy	Sun Mar 20 22:48:08 2011 +0100
+++ b/src/HOL/TLA/Action.thy	Sun Mar 20 23:07:06 2011 +0100
@@ -12,9 +12,8 @@
 
 (** abstract syntax **)
 
-types
-  'a trfun = "(state * state) => 'a"
-  action   = "bool trfun"
+type_synonym 'a trfun = "(state * state) => 'a"
+type_synonym action   = "bool trfun"
 
 arities prod :: (world, world) world
 

--- a/src/HOL/TLA/Init.thy	Sun Mar 20 22:48:08 2011 +0100
+++ b/src/HOL/TLA/Init.thy	Sun Mar 20 23:07:06 2011 +0100
@@ -14,8 +14,7 @@
 typedecl behavior
 arities behavior :: world
 
-types
-  temporal = "behavior form"
+type_synonym temporal = "behavior form"
 
 
 consts

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

--- a/src/HOL/TLA/Memory/MemClerk.thy	Sun Mar 20 22:48:08 2011 +0100
+++ b/src/HOL/TLA/Memory/MemClerk.thy	Sun Mar 20 23:07:06 2011 +0100
@@ -8,11 +8,10 @@
 imports Memory RPC MemClerkParameters
 begin
 
-types
-  (* The clerk takes the same arguments as the memory and sends requests to the RPC *)
-  mClkSndChType = "memChType"
-  mClkRcvChType = "rpcSndChType"
-  mClkStType    = "(PrIds => mClkState) stfun"
+(* The clerk takes the same arguments as the memory and sends requests to the RPC *)
+type_synonym mClkSndChType = "memChType"
+type_synonym mClkRcvChType = "rpcSndChType"
+type_synonym mClkStType = "(PrIds => mClkState) stfun"
 
 definition
   (* state predicates *)

--- a/src/HOL/TLA/Memory/MemClerkParameters.thy	Sun Mar 20 22:48:08 2011 +0100
+++ b/src/HOL/TLA/Memory/MemClerkParameters.thy	Sun Mar 20 23:07:06 2011 +0100
@@ -10,11 +10,10 @@
 
 datatype mClkState = clkA | clkB
 
-types
-  (* types sent on the clerk's send and receive channels are argument types
-     of the memory and the RPC, respectively *)
-  mClkSndArgType   = "memOp"
-  mClkRcvArgType   = "rpcOp"
+(* types sent on the clerk's send and receive channels are argument types
+   of the memory and the RPC, respectively *)
+type_synonym mClkSndArgType = "memOp"
+type_synonym mClkRcvArgType = "rpcOp"
 
 definition
   (* translate a memory call to an RPC call *)

--- a/src/HOL/TLA/Memory/Memory.thy	Sun Mar 20 22:48:08 2011 +0100
+++ b/src/HOL/TLA/Memory/Memory.thy	Sun Mar 20 23:07:06 2011 +0100
@@ -8,10 +8,9 @@
 imports MemoryParameters ProcedureInterface
 begin
 
-types
-  memChType  = "(memOp, Vals) channel"
-  memType = "(Locs => Vals) stfun"      (* intention: MemLocs => MemVals *)
-  resType = "(PrIds => Vals) stfun"
+type_synonym memChType = "(memOp, Vals) channel"
+type_synonym memType = "(Locs => Vals) stfun"  (* intention: MemLocs => MemVals *)
+type_synonym resType = "(PrIds => Vals) stfun"
 
 consts
   (* state predicates *)

--- 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 *)

--- a/src/HOL/TLA/Memory/ProcedureInterface.thy	Sun Mar 20 22:48:08 2011 +0100
+++ b/src/HOL/TLA/Memory/ProcedureInterface.thy	Sun Mar 20 23:07:06 2011 +0100
@@ -8,15 +8,13 @@
 imports "../TLA" RPCMemoryParams
 begin
 
-typedecl
+typedecl ('a,'r) chan
   (* type of channels with argument type 'a and return type 'r.
      we model a channel as an array of variables (of type chan)
      rather than a single array-valued variable because the
      notation gets a little simpler.
   *)
-  ('a,'r) chan
-types
-  ('a,'r) channel =" (PrIds => ('a,'r) chan) stfun"
+type_synonym ('a,'r) channel =" (PrIds => ('a,'r) chan) stfun"
 
 consts
   (* data-level functions *)

--- a/src/HOL/TLA/Memory/RPC.thy	Sun Mar 20 22:48:08 2011 +0100
+++ b/src/HOL/TLA/Memory/RPC.thy	Sun Mar 20 23:07:06 2011 +0100
@@ -8,10 +8,9 @@
 imports RPCParameters ProcedureInterface Memory
 begin
 
-types
-  rpcSndChType  = "(rpcOp,Vals) channel"
-  rpcRcvChType  = "memChType"
-  rpcStType     = "(PrIds => rpcState) stfun"
+type_synonym rpcSndChType = "(rpcOp,Vals) channel"
+type_synonym rpcRcvChType = "memChType"
+type_synonym rpcStType = "(PrIds => rpcState) stfun"
 
 consts
   (* state predicates *)

--- a/src/HOL/TLA/Memory/RPCMemoryParams.thy	Sun Mar 20 22:48:08 2011 +0100
+++ b/src/HOL/TLA/Memory/RPCMemoryParams.thy	Sun Mar 20 23:07:06 2011 +0100
@@ -8,10 +8,10 @@
 imports Main
 begin
 
-types
-  bit = "bool"   (* Signal wires for the procedure interface.
-                    Defined as bool for simplicity. All I should really need is
-                    the existence of two distinct values. *)
+type_synonym bit = "bool"
+ (* Signal wires for the procedure interface.
+    Defined as bool for simplicity. All I should really need is
+    the existence of two distinct values. *)
 
 (* all of these are simple (HOL) types *)
 typedecl Locs    (* "syntactic" value type *)

--- a/src/HOL/TLA/Stfun.thy	Sun Mar 20 22:48:08 2011 +0100
+++ b/src/HOL/TLA/Stfun.thy	Sun Mar 20 23:07:06 2011 +0100
@@ -13,9 +13,8 @@
 
 arities state :: world
 
-types
-  'a stfun = "state => 'a"
-  stpred  = "bool stfun"
+type_synonym 'a stfun = "state => 'a"
+type_synonym stpred  = "bool stfun"
 
 
 consts