[isabelle-dev] inst_subst_tac vs. 'a set

Makarius makarius at sketis.net
Wed Jan 11 16:12:08 CET 2012

Here is another change from 2008 to be reconsidered:

changeset:   26833:7c3757fccf0e
user:        berghofe
date:        Wed May 07 10:59:48 2008 +0200
files:       src/Provers/hypsubst.ML
Added function for computing instantiation for the subst rule, which is used
in vars_gen_hyp_subst_tac and blast_hyp_subst_tac to avoid problems with
HO unification.

It is probably mainly relevant to Stefan and Larry.


More information about the isabelle-dev mailing list