src/FOLP/hypsubst.ML
2015-07-18 wenzelm 2015-07-18 prefer tactics with explicit context;
2014-03-21 wenzelm 2014-03-21 more qualified names;
2011-05-14 wenzelm 2011-05-14 modernized functor names; tuned;
2011-03-26 wenzelm 2011-03-26 more direct loose_bvar1; tuned; slight re-unification of clone (cf. 47f8bfe0f597);
2010-07-08 haftmann 2010-07-08 tuned titles
2010-05-05 haftmann 2010-05-05 farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
2010-03-13 wenzelm 2010-03-13 removed old CVS Ids; tuned headers;
2009-08-29 wenzelm 2009-08-29 eliminated hard tabs;
2008-05-07 berghofe 2008-05-07 Replaced Pattern.eta_contract_atom by Envir.eta_contract.
1997-07-22 paulson 1997-07-22 Removal of the tactical STATE
1997-03-05 paulson 1997-03-05 Now uses eta_contract_atom for greater speed
1996-01-29 clasohm 1996-01-29 expanded tabs
1995-04-07 lcp 1995-04-07 Local version of (original) hypsubst: needs no simplifier