History log of /seL4-l4v-master/l4v/isabelle/src/FOLP/hypsubst.ML
Revision Date Author Comments
# a4bab154 04-Jan-2019 wenzelm <none@none>

isabelle update -u control_cartouches;


# 7f7de75b 18-Jul-2015 wenzelm <none@none>

prefer tactics with explicit context;


# 2c8d6176 21-Mar-2014 wenzelm <none@none>

more qualified names;


# a6a9e8cb 14-May-2011 wenzelm <none@none>

modernized functor names;
tuned;


# 4ea409fd 26-Mar-2011 wenzelm <none@none>

more direct loose_bvar1;
tuned;
slight re-unification of clone (cf. 47f8bfe0f597);


# dd7c556c 08-Jul-2010 haftmann <none@none>

tuned titles


# 4549e8d1 05-May-2010 haftmann <none@none>

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 =)


# 458a4961 13-Mar-2010 wenzelm <none@none>

removed old CVS Ids;
tuned headers;


# 640af3b4 28-Aug-2009 wenzelm <none@none>

eliminated hard tabs;


# f4c802e5 07-May-2008 berghofe <none@none>

Replaced Pattern.eta_contract_atom by Envir.eta_contract.


# f21d92b1 22-Jul-1997 paulson <none@none>

Removal of the tactical STATE


# 8d506f86 05-Mar-1997 paulson <none@none>

Now uses eta_contract_atom for greater speed


# 8a318c3f 29-Jan-1996 clasohm <none@none>

expanded tabs


# 357ea097 07-Apr-1995 lcp <none@none>

Local version of (original) hypsubst: needs no simplifier