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
description:
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.
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
