| Thu, 20 Sep 2012 02:42:49 +0200 |
blanchet |
provide predicator, define relator
|
file |
diff |
annotate
|
| Thu, 20 Sep 2012 02:42:48 +0200 |
blanchet |
renamed "bnf_fp_util.ML" to "bnf_fp.ML"
|
file |
diff |
annotate
|
| Tue, 18 Sep 2012 11:41:04 +0200 |
blanchet |
further tuned simpset
|
file |
diff |
annotate
|
| Mon, 17 Sep 2012 21:33:12 +0200 |
blanchet |
tuned simpset
|
file |
diff |
annotate
|
| Mon, 17 Sep 2012 21:13:30 +0200 |
blanchet |
cleaner way of dealing with the set functions of sums and products
|
file |
diff |
annotate
|
| Mon, 17 Sep 2012 21:13:30 +0200 |
blanchet |
handle the general case with more than two levels of nesting when discharging induction prem prems
|
file |
diff |
annotate
|
| Mon, 17 Sep 2012 21:13:30 +0200 |
blanchet |
clean unfolding of prod and sum sets
|
file |
diff |
annotate
|
| Mon, 17 Sep 2012 21:13:30 +0200 |
blanchet |
got rid of one "auto" in induction tactic
|
file |
diff |
annotate
|
| Sat, 15 Sep 2012 21:10:26 +0200 |
blanchet |
tuned induction tactic
|
file |
diff |
annotate
|
| Sat, 15 Sep 2012 21:10:26 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Fri, 14 Sep 2012 22:23:11 +0200 |
blanchet |
merged two unfold steps
|
file |
diff |
annotate
|
| Fri, 14 Sep 2012 22:23:11 +0200 |
blanchet |
took out one rotate_tac
|
file |
diff |
annotate
|
| Fri, 14 Sep 2012 22:23:11 +0200 |
blanchet |
killed spurious rotate_tac; use auto instead of blast
|
file |
diff |
annotate
|
| Fri, 14 Sep 2012 22:23:11 +0200 |
blanchet |
moved blast tactic to where it is actually needed
|
file |
diff |
annotate
|
| Fri, 14 Sep 2012 22:23:11 +0200 |
blanchet |
correct generalization to 3 or more mutually recursive datatypes
|
file |
diff |
annotate
|
| Fri, 14 Sep 2012 22:23:11 +0200 |
blanchet |
provide more guidance, exploiting our knowledge of the goal
|
file |
diff |
annotate
|
| Fri, 14 Sep 2012 22:23:10 +0200 |
blanchet |
fixed issue with bound variables in prem prems + tuning
|
file |
diff |
annotate
|
| Fri, 14 Sep 2012 22:23:10 +0200 |
blanchet |
use right version of "mk_UnIN"
|
file |
diff |
annotate
|
| Fri, 14 Sep 2012 22:23:10 +0200 |
blanchet |
select the right premise in "mk_induct_discharge_prem_prems_tac" instead of relying on backtracking
|
file |
diff |
annotate
|
| Fri, 14 Sep 2012 22:23:10 +0200 |
blanchet |
tuned code before fixing "mk_induct_discharge_prem_prems_tac"
|
file |
diff |
annotate
|
| Fri, 14 Sep 2012 12:09:27 +0200 |
blanchet |
polished the induction
|
file |
diff |
annotate
|
| Fri, 14 Sep 2012 12:09:27 +0200 |
blanchet |
fixed variable exporting problem
|
file |
diff |
annotate
|
| Fri, 14 Sep 2012 12:09:27 +0200 |
blanchet |
added induct tactic
|
file |
diff |
annotate
|
| Fri, 14 Sep 2012 12:09:27 +0200 |
blanchet |
distinguish between nested and nesting BNFs
|
file |
diff |
annotate
|
| Fri, 14 Sep 2012 12:09:27 +0200 |
blanchet |
make tactic more robust in the case where "asm_simp_tac" already finishes the job
|
file |
diff |
annotate
|
| Tue, 11 Sep 2012 13:06:14 +0200 |
blanchet |
finished splitting sum types for corecursors
|
file |
diff |
annotate
|
| Tue, 11 Sep 2012 13:06:13 +0200 |
blanchet |
first step towards splitting corecursor function arguments into (p, g, h) triples
|
file |
diff |
annotate
|
| Mon, 10 Sep 2012 18:29:55 +0200 |
blanchet |
implemented and use "mk_sum_casesN_balanced"
|
file |
diff |
annotate
|
| Mon, 10 Sep 2012 17:52:01 +0200 |
blanchet |
fixed general case of "mk_sumEN_balanced"
|
file |
diff |
annotate
|
| Mon, 10 Sep 2012 17:36:02 +0200 |
blanchet |
debug
|
file |
diff |
annotate
|
| Sun, 09 Sep 2012 19:57:20 +0200 |
blanchet |
fixed bug with one-value codatatype "codata 'a dead_foo = A"
|
file |
diff |
annotate
|
| Sun, 09 Sep 2012 18:55:10 +0200 |
blanchet |
fixed and reenabled "corecs" theorems
|
file |
diff |
annotate
|
| Sun, 09 Sep 2012 17:14:39 +0200 |
blanchet |
fixed and enabled generation of "coiters" theorems, including the recursive case
|
file |
diff |
annotate
|
| 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
|