[isabelle] "using [[...]]" with Isabelle/Eisbach or Isabelle/ML



Dear all,

what is the equivalent to e.g.

lemma "..."
  ...
  using [[simproc del: s]]
  ...

in Eisbach methods (or if that doesn't work with Isabelle/ML).

cheers

chris




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