[isabelle-dev] NEWS

Makarius makarius at sketis.net
Mon Jun 16 22:22:45 CEST 2008

* ML: rules and tactics that read instantiations (read_instantiate,
res_inst_tac, thin_tac, subgoal_tac etc.) now demand a proper proof
context, which is required for parsing and type-checking.  Moreover,
the variables are specified as plain indexnames, not string encodings

More information about the isabelle-dev mailing list