[isabelle] How to understand the example hoare



cl-isabelle-users:
    my problem is about a command in the \src\Hoare\Hoare.thy  .

method_setup vcg = {*
  Method.no_args
    (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?



regards



	


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