Re: [isabelle] "using [[...]]" with Isabelle/Eisbach or Isabelle/ML
The match method can be slightly abused to get the desired effect:
method my_simproc_env methods m =
(match termI in H[simproc del: bad_simproc]:_ â âmâ)
Here the match against the âtermIâ fact only produces one result, which we name and then use as a handle for making our âsimproc del:â declaration.
We can then use this as a usual higher-order method:
apply (my_simproc_env âsimpâ)
However, it is relatively straightforward to write a method in ML that will accomplish this a bit more generically.
method_setup noting =
âScan.lift (Parse.and_list1 Parse.xthms1 --| Args.$$$ "in") -- Method_Closure.method_text >> (fn (args, m) => fn ctxt =>
fun no_binding args = map (pair (Binding.empty, )) args;
val ctxt' = ctxt
|> Proof_Context.note_thmss ""
(Attrib.map_facts_refs (map (Attrib.attribute_cmd ctxt)) (Proof_Context.get_fact ctxt) (no_binding args))
in Method_Closure.method_evaluate m ctxt' end)
Which then looks a bit like the ânoteâ command:
apply (noting [[simproc del: bad_simproc]]
> On 23 Mar 2016, at 12:39 AM, Christian Sternagel <c.sternagel at gmail.com> wrote:
> 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).
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and