equal
deleted
inserted
replaced
36 "--->" :: "[comb,comb] => bool" (infixl 50) |
36 "--->" :: "[comb,comb] => bool" (infixl 50) |
37 |
37 |
38 translations |
38 translations |
39 "x -1-> y" == "(x,y) \<in> contract" |
39 "x -1-> y" == "(x,y) \<in> contract" |
40 "x ---> y" == "(x,y) \<in> contract^*" |
40 "x ---> y" == "(x,y) \<in> contract^*" |
|
41 |
|
42 syntax (xsymbols) |
|
43 "op ##" :: "[comb,comb] => comb" (infixl "\<bullet>" 90) |
41 |
44 |
42 inductive contract |
45 inductive contract |
43 intros |
46 intros |
44 K: "K##x##y -1-> x" |
47 K: "K##x##y -1-> x" |
45 S: "S##x##y##z -1-> (x##z)##(y##z)" |
48 S: "S##x##y##z -1-> (x##z)##(y##z)" |