Wed, 05 Sep 2012 11:08:18 +0200 | blanchet | tell "select_prem_tac" not to thin any further premisses -- the "rotate_tac" otherwise confuses it | file | diff | annotate |
Wed, 05 Sep 2012 11:08:18 +0200 | blanchet | don't get confused by extraneous premisses | file | diff | annotate |
Tue, 04 Sep 2012 23:42:33 +0200 | blanchet | fixed some type issues in sugar "exhaust_tac" | file | diff | annotate |
Tue, 04 Sep 2012 18:49:40 +0200 | blanchet | implemented "mk_case_tac" -- and got rid of "cheat_tac" | file | diff | annotate |
Tue, 04 Sep 2012 16:27:27 +0200 | blanchet | implemented "mk_half_distinct_tac" | file | diff | annotate |
Tue, 04 Sep 2012 16:17:22 +0200 | blanchet | implemented "mk_inject_tac" | file | diff | annotate |
Tue, 04 Sep 2012 15:51:32 +0200 | blanchet | implemented "mk_exhaust_tac" | file | diff | annotate |
Tue, 04 Sep 2012 13:06:41 +0200 | blanchet | more work on sugar + simplify Trueprop + eq idiom everywhere | file | diff | annotate |