Hi,
I want to prove a goal like this:
`case "d" of "u" =>1 |"s" =>2|"d" =>3
|"p" =>4`
Is there a tactic which can match "d" with the branch "d" and then execute this
branch.------------------------------------------------------------------------------
_______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
