src/HOL/Library/Quotient_Set.thy
Fri, 20 Apr 2012 15:34:33 +0200 huffman move definition of set_rel into Library/Quotient_Set.thy
Fri, 13 Apr 2012 14:00:26 +0200 wenzelm updated headers;
Tue, 03 Apr 2012 16:26:48 +0200 kuncar new package Lifting - initial commit
Fri, 23 Mar 2012 14:20:09 +0100 kuncar store the relational theorem for every relator
Sat, 24 Dec 2011 15:53:10 +0100 haftmann adjusted to set/pred distinction by means of type constructor `set`
Sat, 10 Sep 2011 22:43:17 +0200 krauss mem_prs and mem_rsp in accordance with sets-as-predicates representation (backported from AFP/Coinductive)
Wed, 24 Aug 2011 10:59:22 +0900 Cezary Kaliszyk Quotient Package: add mem_rsp, mem_prs, tune proofs.
Tue, 23 Aug 2011 03:34:17 +0900 Cezary Kaliszyk Quotient Package: some infrastructure for lifting inside sets
less more (0) tip