[isabelle-dev] NEWS: instantiation rules
makarius at sketis.net
Mon Jul 27 22:36:10 CEST 2015
* 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.
More information about the isabelle-dev