src/HOL/HOLCF/FOCUS/Fstreams.thy
changeset 41476 0fa9629aa399
parent 41431 138f414f14cb
child 41855 c3b6e69da386
--- a/src/HOL/HOLCF/FOCUS/Fstreams.thy	Sat Jan 08 00:28:31 2011 +0100
+++ b/src/HOL/HOLCF/FOCUS/Fstreams.thy	Sat Jan 08 09:30:52 2011 -0800
@@ -12,7 +12,7 @@
 
 default_sort type
 
-types 'a fstream = "('a lift) stream"
+type_synonym 'a fstream = "('a lift) stream"
 
 definition
   fsingleton    :: "'a => 'a fstream"  ("<_>" [1000] 999) where