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