src/HOL/Nominal/Examples/Crary.thy
Fri, 02 Feb 2007 17:16:16 +0100 urbanc added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
Wed, 17 Jan 2007 19:29:55 +0100 urbanc tuned a bit the proofs
Tue, 16 Jan 2007 13:59:08 +0100 urbanc formalisation of Crary's chapter on logical relations
less more (0) tip