equal
deleted
inserted
replaced
31 |
31 |
32 datatype |
32 datatype |
33 |
33 |
34 State = Sd D | Snil ("\<currency>") |
34 State = Sd D | Snil ("\<currency>") |
35 |
35 |
36 types |
36 type_synonym |
37 |
|
38 SPF11 = "M fstream \<rightarrow> D fstream" |
37 SPF11 = "M fstream \<rightarrow> D fstream" |
|
38 |
|
39 type_synonym |
39 SPEC11 = "SPF11 set" |
40 SPEC11 = "SPF11 set" |
|
41 |
|
42 type_synonym |
40 SPSF11 = "State \<Rightarrow> SPF11" |
43 SPSF11 = "State \<Rightarrow> SPF11" |
|
44 |
|
45 type_synonym |
41 SPECS11 = "SPSF11 set" |
46 SPECS11 = "SPSF11 set" |
42 |
47 |
43 definition |
48 definition |
44 BufEq_F :: "SPEC11 \<Rightarrow> SPEC11" where |
49 BufEq_F :: "SPEC11 \<Rightarrow> SPEC11" where |
45 "BufEq_F B = {f. \<forall>d. f\<cdot>(Md d\<leadsto><>) = <> \<and> |
50 "BufEq_F B = {f. \<forall>d. f\<cdot>(Md d\<leadsto><>) = <> \<and> |