[isabelle] small verification task

Dear All:

Is it possible to write a small piece of code in SML, say, to compute
the GCD of 2 given numbers, and use Isabelle and its induction tactic
to directly verify the correctness of this very code?  Anyone would
kindly point to examples where this has been done?


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