equal
deleted
inserted
replaced
64 | PD "name" "name" |
64 | PD "name" "name" |
65 binder |
65 binder |
66 f::"pat' \<Rightarrow> atom set" |
66 f::"pat' \<Rightarrow> atom set" |
67 where |
67 where |
68 "f PN = {}" |
68 "f PN = {}" |
|
69 | "f (PD x y) = {atom x, atom y}" |
69 | "f (PS x) = {atom x}" |
70 | "f (PS x) = {atom x}" |
70 | "f (PD x y) = {atom x, atom y}" |
71 |
71 |
72 |
72 (* compat should be |
73 (* compat should be |
73 compat (PN) pi (PN) == True |
74 compat (PN) pi (PN) == True |
74 compat (PS x) pi (PS x') == pi o x = x' |
75 compat (PS x) pi (PS x') == pi o x = x' |
75 compat (PD p1 p2) pi (PD p1' p2') == compat p1 pi p1' & compat p2 pi p2' |
76 compat (PD p1 p2) pi (PD p1' p2') == compat p1 pi p1' & compat p2 pi p2' |