equal
deleted
inserted
replaced
657 |
657 |
658 |
658 |
659 (* example with a bn function defined over the type itself *) |
659 (* example with a bn function defined over the type itself *) |
660 datatype rtrm6 = |
660 datatype rtrm6 = |
661 rVr6 "name" |
661 rVr6 "name" |
662 | rLm6 "name" "rtrm6" |
662 | rLm6 "name" "rtrm6" --"bind name in rtrm6" |
663 | rLt6 "rtrm6" "rtrm6" --"bind (bv6 left) in (right)" |
663 | rLt6 "rtrm6" "rtrm6" --"bind (bv6 left) in (right)" |
664 |
664 |
665 primrec |
665 primrec |
666 rbv6 |
666 rbv6 |
667 where |
667 where |