--- a/src/HOLCF/FOCUS/Fstream.thy Tue Sep 06 20:53:27 2005 +0200
+++ b/src/HOLCF/FOCUS/Fstream.thy Tue Sep 06 21:51:17 2005 +0200
@@ -1,45 +1,49 @@
-(* Title: HOLCF/FOCUS/Fstream.thy
+(* Title: HOLCF/FOCUS/Fstream.thy
ID: $Id$
- Author: David von Oheimb, TU Muenchen
+ Author: David von Oheimb, TU Muenchen
FOCUS streams (with lifted elements)
###TODO: integrate Fstreams.thy
*)
-(* FOCUS flat streams *)
-
-Fstream = Stream +
+header {* FOCUS flat streams *}
-default type
+theory Fstream
+imports Stream
+begin
-types 'a fstream = ('a lift) stream
+defaultsort type
+
+types 'a fstream = "'a lift stream"
consts
- fscons :: "'a \\<Rightarrow> 'a fstream \\<rightarrow> 'a fstream"
- fsfilter :: "'a set \\<Rightarrow> 'a fstream \\<rightarrow> 'a fstream"
+ fscons :: "'a \<Rightarrow> 'a fstream \<rightarrow> 'a fstream"
+ fsfilter :: "'a set \<Rightarrow> 'a fstream \<rightarrow> 'a fstream"
syntax
- "@emptystream":: "'a fstream" ("<>")
- "@fscons" :: "'a \\<Rightarrow> 'a fstream \\<Rightarrow> 'a fstream" ("(_~>_)" [66,65] 65)
- "@fsfilter" :: "'a set \\<Rightarrow> 'a fstream \\<Rightarrow> 'a fstream" ("(_'(C')_)" [64,63] 63)
+ "@emptystream":: "'a fstream" ("<>")
+ "@fscons" :: "'a \<Rightarrow> 'a fstream \<Rightarrow> 'a fstream" ("(_~>_)" [66,65] 65)
+ "@fsfilter" :: "'a set \<Rightarrow> 'a fstream \<Rightarrow> 'a fstream" ("(_'(C')_)" [64,63] 63)
syntax (xsymbols)
- "@fscons" :: "'a \\<Rightarrow> 'a fstream \\<Rightarrow> 'a fstream" ("(_\\<leadsto>_)"
- [66,65] 65)
- "@fsfilter" :: "'a set \\<Rightarrow> 'a fstream \\<Rightarrow> 'a fstream" ("(_\\<copyright>_)"
- [64,63] 63)
+ "@fscons" :: "'a \<Rightarrow> 'a fstream \<Rightarrow> 'a fstream" ("(_\<leadsto>_)"
+ [66,65] 65)
+ "@fsfilter" :: "'a set \<Rightarrow> 'a fstream \<Rightarrow> 'a fstream" ("(_\<copyright>_)"
+ [64,63] 63)
translations
- "<>" => "\\<bottom>"
- "a~>s" == "fscons a\\<cdot>s"
- "A(C)s" == "fsfilter A\\<cdot>s"
+ "<>" => "\<bottom>"
+ "a~>s" == "fscons a\<cdot>s"
+ "A(C)s" == "fsfilter A\<cdot>s"
defs
- fscons_def "fscons a \\<equiv> \\<Lambda> s. Def a && s"
- fsfilter_def "fsfilter A \\<equiv> sfilter\\<cdot>(flift2 (\\<lambda>x. x\\<in>A))"
+ fscons_def: "fscons a \<equiv> \<Lambda> s. Def a && s"
+ fsfilter_def: "fsfilter A \<equiv> sfilter\<cdot>(flift2 (\<lambda>x. x\<in>A))"
+
+ML {* use_legacy_bindings (the_context ()) *}
end