Mon, 03 Mar 2014 12:48:20 +0100 | blanchet | make 'diff_iff' a simp rule if available | changeset | files |
Mon, 03 Mar 2014 12:48:20 +0100 | blanchet | less aggressive resolving | changeset | files |
Mon, 03 Mar 2014 12:48:20 +0100 | blanchet | repaired argument list to corecursor | changeset | files |
Mon, 03 Mar 2014 12:48:20 +0100 | blanchet | adapted to absence of 'unfold' | changeset | files |
Mon, 03 Mar 2014 12:48:20 +0100 | blanchet | got rid of automatically generated fold constant and theorems (to reduce overhead) | changeset | files |
Mon, 03 Mar 2014 12:48:20 +0100 | blanchet | use same identity function for abs and rep (doesn't seem to confuse any proofs) | changeset | files |