Fri, 26 Aug 2011 21:11:23 +0200 | haftmann | separating predicates and sets syntactically | changeset | files |
Fri, 26 Aug 2011 18:24:22 +0200 | haftmann | merged | changeset | files |
Fri, 26 Aug 2011 18:23:33 +0200 | haftmann | avoid intermixing set and predicates; dropped lemmas mem_rsp and mem_prs (now in Quotient_Set.thy) | changeset | files |