* 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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
