equal
deleted
inserted
replaced
924 apply (subst alpha5_INJ(5)) |
924 apply (subst alpha5_INJ(5)) |
925 apply (simp add: distinct_helper2) |
925 apply (simp add: distinct_helper2) |
926 done |
926 done |
927 |
927 |
928 |
928 |
929 |
929 (* example with a bn function defined over the type itself *) |
930 |
|
931 |
|
932 |
|
933 |
|
934 datatype rtrm6 = |
930 datatype rtrm6 = |
935 rVr6 "name" |
931 rVr6 "name" |
936 | rAp6 "rtrm6" "rtrm6" |
932 | rAp6 "rtrm6" "rtrm6" |
937 | rFo6 "rtrm6" "rtrm6" --"bind (bv6 left) in (right)" |
933 | rFo6 "rtrm6" "rtrm6" --"bind (bv6 left) in (right)" |
938 |
934 |