Email Gateway (Aug 22 2022 at 13:12): Email Gateway (Aug 22 2022 at 13:12):From: nemouchi <Yakoub.Nemouchi@lri.fr>
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,
Yakoub.
Email Gateway (Aug 22 2022 at 13:12):From: Makarius <makarius@sketis.net>
On Mon, 25 Apr 2016, nemouchi wrote:
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.
Explanations of user-relevant changes are in the NEWS file. Something not
mentioned there is not sufficiently relevant, or it was just forgotten. In
any case, it also helps to use "hg grep --all" on the Isabelle Mercurial
history, i.e. the proof behind the present state of the sources.
Isabelle 2013-2 Isabelle 2016
Drule.cterm_fun ----> ?
Drule.ctyp_fun ----> ?
Obsolete. In the rare cases where ctyp or cterm values are really
required, you can use Thm.term_of / Thm.cterm_of etc. explicitly.
Drule.instantiate_normalize ----> ?
It still exists, although it is a bit old-fashioned. The NEWS file has
this entry:
Instantiation rules have been re-organized as follows:
Thm.instantiate (low-level instantiation with named arguments)
Thm.instantiate' (version with positional arguments)
Drule.infer_instantiate (instantiation with type inference)
Drule.infer_instantiate' (version with positional arguments)
The LHS only requires variable specifications, instead of full terms.
Old cterm_instantiate is superseded by infer_instantiate.
INCOMPATIBILITY, need to re-adjust some ML names and types accordingly.
Thm.nprems_of ----> ?
Still exists, unchanged.
Such low-level inspection of goal states are rarely seen in practice. It
is more likely that you want to use tacticals like SUBGOAL, SELECT_GOAL,
PREFER_GOAL, SUBPROOF.
Pure.cpat ----> ?
(cpat was an antiquotation!!)
It was last use for instantiation operations, but that was simplified as
explained in the NEWS item above.
Unlikely that @{cpat} it is still needed today. It indicates some old /
obsolete practice.
Makarius
Last updated: May 06 2024 at 12:29 UTC