[isabelle] Object-reasoning


Is it correct to say that there's object-level reasoning done in
Isabelle? It seems that each step in an object-level proof is written
using meta-level notations. Does that mean proving an object-level
sentence involves only meta-level reasoning?

Thanks a lot for your time.


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