[isabelle] Going from Isabelle 2013 to Isabelle 2016
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
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
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!!)
This archive was generated by a fusion of
Pipermail (Mailman edition) and