Re: [isabelle] On Recursion Induction

On 08.05.2012 07:01, Christian Sternagel wrote:
declare [[goals_limit=20]]

when in theory mode (i.e., not inside a proof), or like

note [[goals_limit=20]]

when in proof mode. (I don't know if it is possible to set it in "prove"
mode however ;)).

This should be "using [[goals_limit=20]]]" then.

  -- Lars

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.