| Fri, 30 Aug 2013 14:17:19 +0200 |
blanchet |
more canonical naming
|
file |
diff |
annotate
|
| Thu, 29 Aug 2013 23:01:04 +0200 |
blanchet |
renamed BNF fact
|
file |
diff |
annotate
|
| Thu, 29 Aug 2013 22:39:46 +0200 |
blanchet |
renamed BNF fact
|
file |
diff |
annotate
|
| Mon, 12 Aug 2013 15:25:17 +0200 |
blanchet |
define case constant from other 'free constructor' axioms
|
file |
diff |
annotate
|
| Mon, 12 Aug 2013 15:25:16 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Mon, 15 Jul 2013 14:23:51 +0200 |
traytel |
eliminate duplicated theorems (thanks to "Auto solve_direct" in jEdit)
|
file |
diff |
annotate
|
| Fri, 07 Jun 2013 17:04:55 +0100 |
blanchet |
code simplifications (cf. 78a3d5006cf1)
|
file |
diff |
annotate
|
| Fri, 07 Jun 2013 14:45:07 +0200 |
blanchet |
changed back type of corecursor for nested case, effectively reverting aa66ea552357 and 78a3d5006cf1
|
file |
diff |
annotate
|
| Thu, 06 Jun 2013 21:18:39 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Thu, 06 Jun 2013 21:12:08 +0200 |
blanchet |
fixed failure in coinduction rule tactic
|
file |
diff |
annotate
|
| Thu, 30 May 2013 12:56:25 +0200 |
wenzelm |
stay within regular tactic language -- avoid operating on whole proof state;
|
file |
diff |
annotate
|
| Wed, 29 May 2013 02:35:49 +0200 |
blanchet |
generalized recursors, effectively reverting inductive half of c7a034d01936
|
file |
diff |
annotate
|
| Tue, 28 May 2013 08:36:12 +0200 |
blanchet |
clean up list of theorems
|
file |
diff |
annotate
|
| Tue, 28 May 2013 08:36:11 +0200 |
blanchet |
removed needless comment (yes, sum_case_if is needed)
|
file |
diff |
annotate
|
| Tue, 07 May 2013 14:22:54 +0200 |
traytel |
got rid of the set based relator---use (binary) predicate based relator instead
|
file |
diff |
annotate
|
| Wed, 01 May 2013 19:33:49 +0200 |
blanchet |
renamed a few FP-related files, to make it clear that these are not the sum of LFP + GFP but rather shared basic libraries
|
file |
diff |
annotate
|
| Tue, 30 Apr 2013 16:42:23 +0200 |
blanchet |
rationalized terminology (iterator = fold or rec, xxfoo = (co)foo or (un)foo)
|
file |
diff |
annotate
|
| Sat, 27 Apr 2013 20:50:20 +0200 |
wenzelm |
uniform Proof.context for hyp_subst_tac;
|
file |
diff |
annotate
|
| Wed, 24 Apr 2013 17:47:22 +0200 |
blanchet |
renamed "set_natural" to "set_map", reflecting {Bl,Po,Tr} concensus
|
file |
diff |
annotate
|
| Thu, 18 Apr 2013 17:07:01 +0200 |
wenzelm |
simplifier uses proper Proof.context instead of historic type simpset;
|
file |
diff |
annotate
|
| Tue, 02 Oct 2012 01:00:18 +0200 |
blanchet |
continued changing type of corec type
|
file |
diff |
annotate
|
| Tue, 02 Oct 2012 01:00:18 +0200 |
blanchet |
made (co)rec tactic more robust when the simplifier succeeds early
|
file |
diff |
annotate
|
| Mon, 01 Oct 2012 11:04:30 +0200 |
blanchet |
fixed recursor definition for datatypes with inner products (e.g. "'a trm" from the lambda-term example)
|
file |
diff |
annotate
|
| Mon, 01 Oct 2012 10:46:30 +0200 |
blanchet |
tweaked corecursor/coiterator tactic
|
file |
diff |
annotate
|
| Mon, 01 Oct 2012 10:34:58 +0200 |
blanchet |
changed the type of the recursor for nested recursion
|
file |
diff |
annotate
|
| Sun, 30 Sep 2012 22:02:34 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Sun, 30 Sep 2012 12:04:13 +0200 |
traytel |
tuned tactic
|
file |
diff |
annotate
|
| Fri, 28 Sep 2012 15:23:32 +0200 |
blanchet |
simplified simpset
|
file |
diff |
annotate
|
| Fri, 28 Sep 2012 15:14:11 +0200 |
blanchet |
fixed simplification of prod and sum relators to avoid issues with e.g. codata ('a, 'b) k = K "'a + 'b"
|
file |
diff |
annotate
|
| Fri, 28 Sep 2012 11:31:51 +0200 |
traytel |
tuned tactic
|
file |
diff |
annotate
|
| Fri, 28 Sep 2012 09:38:07 +0200 |
traytel |
tuned tactic
|
file |
diff |
annotate
|
| Fri, 28 Sep 2012 09:12:50 +0200 |
blanchet |
renamed ML file in preparation for next step
|
file |
diff |
annotate
| base
|