NEWS;
authorwenzelm
Mon Jul 27 17:56:08 2015 +0200 (2015-07-27)
changeset 60802067658d63c5d
parent 60801 7664e0916eec
child 60803 e11f47dd0786
NEWS;
NEWS
     1.1 --- a/NEWS	Mon Jul 27 17:44:55 2015 +0200
     1.2 +++ b/NEWS	Mon Jul 27 17:56:08 2015 +0200
     1.3 @@ -246,6 +246,18 @@
     1.4  
     1.5  *** ML ***
     1.6  
     1.7 +* Instantiation rules have been re-organized as follows:
     1.8 +
     1.9 +  Thm.instantiate  (*low-level instantiation with named arguments*)
    1.10 +  Thm.instantiate' (*version with positional arguments*)
    1.11 +
    1.12 +  Drule.infer_instantiate  (*instantiation with type inference*)
    1.13 +  Drule.infer_instantiate'  (*version with positional arguments*)
    1.14 +
    1.15 +The LHS only requires variable specifications, instead of full terms.
    1.16 +Old cterm_instantiate is superseded by infer_instantiate.
    1.17 +INCOMPATIBILITY, need to re-adjust some ML names and types accordingly.
    1.18 +
    1.19  * Old tactic shorthands atac, rtac, etac, dtac, ftac have been
    1.20  discontinued. INCOMPATIBILITY, use regular assume_tac, resolve_tac etc.
    1.21  instead (with proper context).