| Thu, 02 Jan 2014 21:35:21 +0100 | blanchet | made tactic more robust | changeset | files |
| Thu, 02 Jan 2014 20:51:09 +0100 | blanchet | made tactic handle corner cases, where some of the 'disc' properties are missing, correctly | changeset | files |
| Thu, 02 Jan 2014 20:25:40 +0100 | blanchet | simplified code | changeset | files |
| Thu, 02 Jan 2014 20:10:08 +0100 | blanchet | prevent tactic from getting out of sync and wrongly attack next subgoal | changeset | files |
| Thu, 02 Jan 2014 19:07:36 +0100 | blanchet | removed pointless warning (cf. http://stackoverflow.com/questions/20233463/isabelle-metis-proof-state-contains-the-universal-sort/20785045#20785045) | changeset | files |
| Thu, 02 Jan 2014 09:50:22 +0100 | blanchet | consider code as exhaustive | changeset | files |