Re: [isabelle] tacticals, functionality of ORELSE
When testtac1 is called, ML evaluates both arguments of ORELSE, which
are tactic-valued expressions. The second argument raises exception
Match before ORELSE is even called.
On 28 Aug 2006, at 09:34, Alexander Sauerbier wrote:
If I understand it correctly, /testtac1/ should do exactly the same
as /testtac/, because ORELSE should just try the tactic on
operator's left side and ignore the tactic on the right side... but
obviously I didn't understand it correctly.
Can you give me some hints, please?
This archive was generated by a fusion of
Pipermail (Mailman edition) and