[isabelle-dev] NEWS: instantiation rules

[Makarius]

* 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.


This refers to Isabelle/067658d63c5d.  I've made a full round through 
Isabelle + AFP to re-integrate the different variations on 
Drule.cterm_instantiate that have shown up in many years. Hopefully we are 
now back to a stable state of canonical operations.


 	Makarius