src/HOL/TLA/Init.thy
changeset 42018 878f33040280
parent 35318 e1b61c5fd494
child 55382 9218fa411c15
     1.1 --- a/src/HOL/TLA/Init.thy	Sun Mar 20 22:48:08 2011 +0100
     1.2 +++ b/src/HOL/TLA/Init.thy	Sun Mar 20 23:07:06 2011 +0100
     1.3 @@ -14,8 +14,7 @@
     1.4  typedecl behavior
     1.5  arities behavior :: world
     1.6  
     1.7 -types
     1.8 -  temporal = "behavior form"
     1.9 +type_synonym temporal = "behavior form"
    1.10  
    1.11  
    1.12  consts