[isabelle] How to understand the example hoare

    my problem is about a command in the \src\Hoare\Hoare.thy  .

method_setup vcg = {*
    (Method.SIMPLE_METHOD' HEADGOAL (hoare_tac (K all_tac))) *}
  "verification condition generator"

where do I find the semantical explanation about this command.

Especially what is "K"?

This example is too difficult for me.

who write the example or understand it, and can you give some helpful 
suggestion to read it?



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