Re: [isabelle] Going from Isabelle 2013 to Isabelle 2016

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.


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