| Thu, 25 Aug 2011 14:06:34 +0200 | krauss | lemma Compl_insert: "- insert x A = (-A) - {x}" | changeset | files |
| Thu, 25 Aug 2011 11:15:31 +0200 | boehmes | avoid variable clashes by properly incrementing indices | changeset | files |
| Thu, 25 Aug 2011 11:15:31 +0200 | boehmes | improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization | changeset | files |