Fri, 20 Apr 2012 15:34:33 +0200 | huffman | move definition of set_rel into Library/Quotient_Set.thy | file | diff | annotate |
Fri, 13 Apr 2012 14:00:26 +0200 | wenzelm | updated headers; | file | diff | annotate |
Tue, 03 Apr 2012 16:26:48 +0200 | kuncar | new package Lifting - initial commit | file | diff | annotate |
Fri, 23 Mar 2012 14:20:09 +0100 | kuncar | store the relational theorem for every relator | file | diff | annotate |
Sat, 24 Dec 2011 15:53:10 +0100 | haftmann | adjusted to set/pred distinction by means of type constructor `set` | file | diff | annotate |
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) | file | diff | annotate |
Wed, 24 Aug 2011 10:59:22 +0900 | Cezary Kaliszyk | Quotient Package: add mem_rsp, mem_prs, tune proofs. | file | diff | annotate |
Tue, 23 Aug 2011 03:34:17 +0900 | Cezary Kaliszyk | Quotient Package: some infrastructure for lifting inside sets | file | diff | annotate |