Theorems for converting between wf and wfP are now declared
as hints.
(* Title: Pure/CPure.thy ID: $Id$The CPure theory -- Pure with alternative application syntax.*)theory CPureimports Purebeginsetup -- {* Some syntax modifications, see ROOT.ML *}end