# HG changeset patch
# User wenzelm
# Date 1295188007 -3600
# Node ID e13df75fee79d7e49c4f47d1c873d1b3eccf17ba
# Parent  1f930561a560caffd6e3197461e5ee796820ebcc
type_synonym;

diff -r 1f930561a560 -r e13df75fee79 src/HOL/SPARK/Examples/RIPEMD-160/RMD.thy
--- a/src/HOL/SPARK/Examples/RIPEMD-160/RMD.thy	Sun Jan 16 15:04:16 2011 +0100
+++ b/src/HOL/SPARK/Examples/RIPEMD-160/RMD.thy	Sun Jan 16 15:26:47 2011 +0100
@@ -11,12 +11,12 @@
 
 (* all operations are defined on 32-bit words *)
 
-types word32 = "32 word"
-types byte = "8 word"
-types perm = "nat \<Rightarrow> nat"
-types chain = "word32 * word32 * word32 * word32 * word32"
-types block = "nat \<Rightarrow> word32"
-types message = "nat \<Rightarrow> block"
+type_synonym word32 = "32 word"
+type_synonym byte = "8 word"
+type_synonym perm = "nat \<Rightarrow> nat"
+type_synonym chain = "word32 * word32 * word32 * word32 * word32"
+type_synonym block = "nat \<Rightarrow> word32"
+type_synonym message = "nat \<Rightarrow> block"
 
 (* nonlinear functions at bit level *)