| Sun, 09 Sep 2012 12:07:15 +0200 |
blanchet |
use map_id, not map_id', to allow better composition
|
file |
diff |
annotate
|
| Sat, 08 Sep 2012 22:54:37 +0200 |
blanchet |
fixed and enabled iterator/recursor theorems
|
file |
diff |
annotate
|
| Sat, 08 Sep 2012 21:04:26 +0200 |
blanchet |
renamed xxxBNF to pre_xxx
|
file |
diff |
annotate
|
| Sat, 08 Sep 2012 21:04:26 +0200 |
blanchet |
fixed handling of map of "fun"
|
file |
diff |
annotate
|
| Sat, 08 Sep 2012 21:04:26 +0200 |
blanchet |
some work on coiter tactic
|
file |
diff |
annotate
|
| Sat, 08 Sep 2012 21:04:26 +0200 |
blanchet |
define corecursors
|
file |
diff |
annotate
|
| Sat, 08 Sep 2012 21:04:26 +0200 |
blanchet |
completed iter/rec proofs
|
file |
diff |
annotate
|
| Sat, 08 Sep 2012 21:04:26 +0200 |
blanchet |
implemented "mk_iter_or_rec_tac"
|
file |
diff |
annotate
|
| Wed, 05 Sep 2012 15:40:29 +0200 |
blanchet |
fixed (n + 1)st bug in "mk_exhaust_tac" -- arose with uncurried constructors
|
file |
diff |
annotate
|
| Wed, 05 Sep 2012 15:40:28 +0200 |
blanchet |
fixed "mk_exhaust_tac" for the nth time
|
file |
diff |
annotate
|
| 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
|