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.

Larry Paulson

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 MHonArc.