[isabelle] Goedel's Proof

Hello all,

now I've got 50 JAVA/C functions similar to

----------- function 1 out of 46 -------------------
  //  1. Proposition
  // x is divisible by y
  BOOL divisible(NAT x, NAT y) {
    NAT i;
    for (i=1;(i<=y);i++)
      if (x==y*z)
        return TRUE;
    return FALSE;}
--------------------- end of function------------------------------

and I don't know how to transpose them into Isabelle proofs/theorems effectively.

Is anyone interested and willing to help me investigate the stuff?


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