Re: [isabelle] tactic being executed twice

> Also, using CSUBGOAL works.  I couldn't understand
> what "Subgoal.FOCUS" does.  CSUBGOAL is similar to SUBGOAL which is
> described clearly in the old Reference Manual.

Subgoal.FOCUS is a very useful combinator. It allows you to destructure
a goal such that you can get your hands on the premises and fixed
variables easily. I found that its type is quite self-explanatory:

  type focus =
   {context: Proof.context, params: (string * cterm) list,
    prems: thm list, asms: cterm list,
    concl: cterm,
    schematics: ((indexname * sort) * ctyp) list * ((indexname * typ) *
cterm) list}

  val FOCUS: (focus -> tactic) -> Proof.context -> int -> tactic

I use it for almost all of my custom ML tactics.


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