[isabelle] Going from Isabelle 2013 to Isabelle 2016

Dear all,

Some of the old ML functions do not have a "direct" translation in the new ML libraries provided with Isabelle 2016 distribution.

Knowing the Isabelle community, i can guess that an explanation is provided somewhere, but

since i do not know very well the structure of Isabelle Kernel i did not found it.

Do Someone know the 2016 versions of this list of functions:

Isabelle 2013-2     Isabelle 2016

Drule.cterm_fun ---->   ?

Drule.ctyp_fun  ---->   ?

Drule.instantiate_normalize ----> ?

(for Drule.instantiate_normalize even the type of the function was changed... explanation?!!)

Thm.nprems_of   ----> ?

(Ok i can re-define it, but well maybe something similar is already existing in the new structure)

Pure.cpat      ----> ?
(cpat was an antiquotation!!)

Kind Regards,


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