Wed, 23 Apr 2014 10:23:27 +0200 | blanchet | localize new size function generation code | changeset | files |
Wed, 23 Apr 2014 10:23:27 +0200 | blanchet | no need to make 'size' generation an interpretation -- overkill | changeset | files |
Wed, 23 Apr 2014 10:23:27 +0200 | blanchet | put theorems in right slot | changeset | files |
Wed, 23 Apr 2014 10:23:27 +0200 | blanchet | manual merge + added 'rel_distincts' field to record for symmetry | changeset | files |
Wed, 23 Apr 2014 10:23:27 +0200 | blanchet | pick up all 'nesting' theorems | changeset | files |
Wed, 23 Apr 2014 10:23:27 +0200 | blanchet | added 'size' of finite sets | changeset | files |
Wed, 23 Apr 2014 10:23:27 +0200 | blanchet | prevent tactic failures by detecting and ignoring BNFs with no 'size' functions early | changeset | files |