On 04/11/14 13:33, ＂f~鳓ぁぇ wrote:
> 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.
SIMP_TAC (srw_ss()) []
or
SRW_TAC[][]
should both work on this sort of goal.
Michael
________________________________
The information in this e-mail may be confidential and subject to legal
professional privilege and/or copyright. National ICT Australia Limited accepts
no liability for any damage caused by this email or its attachments.
------------------------------------------------------------------------------
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
