author | wenzelm |
Sat, 07 Mar 2015 22:38:11 +0100 | |
changeset 59648 | d1148f0baef5 |
parent 59647 | c6f413b660cf |
child 59649 | c4104707385d |
--- a/NEWS Sat Mar 07 21:32:31 2015 +0100 +++ b/NEWS Sat Mar 07 22:38:11 2015 +0100 @@ -6,6 +6,11 @@ *** General *** +* Generated schematic variables in standard format of exported facts are +incremented to avoid material in the proof context. Rare +INCOMPATIBILITY, explicit instantiation sometimes needs to refer to +different index. + * Commands 'method_setup' and 'attribute_setup' now work within a local theory context.