# HG changeset patch
# User wenzelm
# Date 1295111546 -3600
# Node ID 4031fb078acc53767ca0c2dd1f3128769d5d56e3
# Parent  f5e7f671281520d686f4d4415aad117962d3c021
type_synonym;

diff -r f5e7f6712815 -r 4031fb078acc src/HOL/Unix/Unix.thy
--- a/src/HOL/Unix/Unix.thy	Sat Jan 15 17:32:07 2011 +0100
+++ b/src/HOL/Unix/Unix.thy	Sat Jan 15 18:12:26 2011 +0100
@@ -47,10 +47,9 @@
   names and user ids as would be present in a reality.
 *}
 
-types
-  uid = nat
-  name = nat
-  path = "name list"
+type_synonym uid = nat
+type_synonym name = nat
+type_synonym path = "name list"
 
 
 subsection {* Attributes *}
@@ -80,7 +79,7 @@
   | Writable
   | Executable    -- "(ignored)"
 
-types perms = "perm set"
+type_synonym perms = "perm set"
 
 record att =
   owner :: uid
@@ -132,8 +131,7 @@
   of directory nodes).
 *}
 
-types
-  "file" = "(att \<times> string, att, name) env"
+type_synonym "file" = "(att \<times> string, att, name) env"
 
 text {*
   \medskip The HOL library also provides @{term lookup} and @{term