Wed, 18 Sep 2013 15:33:30 +0200 |
avoid duplicate simp rule warnings
|
file | diff | annotate |
Thu, 12 Sep 2013 17:36:06 +0200 |
made tactic handle gracefully the case: codatatype ('a, 's) scheduler2 = Combine2 "'s => 'a" "'s => ('a, 's) scheduler2"
|
file | diff | annotate |
Fri, 30 Aug 2013 14:17:19 +0200 |
more canonical naming
|
file | diff | annotate |
Thu, 29 Aug 2013 23:01:04 +0200 |
renamed BNF fact
|
file | diff | annotate |
Thu, 29 Aug 2013 22:39:46 +0200 |
renamed BNF fact
|
file | diff | annotate |
Mon, 12 Aug 2013 15:25:17 +0200 |
define case constant from other 'free constructor' axioms
|
file | diff | annotate |
Mon, 12 Aug 2013 15:25:16 +0200 |
tuning
|
file | diff | annotate |
Mon, 15 Jul 2013 14:23:51 +0200 |
eliminate duplicated theorems (thanks to "Auto solve_direct" in jEdit)
|
file | diff | annotate |
Fri, 07 Jun 2013 17:04:55 +0100 |
code simplifications (cf. 78a3d5006cf1)
|
file | diff | annotate |
Fri, 07 Jun 2013 14:45:07 +0200 |
changed back type of corecursor for nested case, effectively reverting aa66ea552357 and 78a3d5006cf1
|
file | diff | annotate |
Thu, 06 Jun 2013 21:18:39 +0200 |
tuning
|
file | diff | annotate |
Thu, 06 Jun 2013 21:12:08 +0200 |
fixed failure in coinduction rule tactic
|
file | diff | annotate |
Thu, 30 May 2013 12:56:25 +0200 |
stay within regular tactic language -- avoid operating on whole proof state;
|
file | diff | annotate |
Wed, 29 May 2013 02:35:49 +0200 |
generalized recursors, effectively reverting inductive half of c7a034d01936
|
file | diff | annotate |
Tue, 28 May 2013 08:36:12 +0200 |
clean up list of theorems
|
file | diff | annotate |
Tue, 28 May 2013 08:36:11 +0200 |
removed needless comment (yes, sum_case_if is needed)
|
file | diff | annotate |
Tue, 07 May 2013 14:22:54 +0200 |
got rid of the set based relator---use (binary) predicate based relator instead
|
file | diff | annotate |
Wed, 01 May 2013 19:33:49 +0200 |
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 |
rationalized terminology (iterator = fold or rec, xxfoo = (co)foo or (un)foo)
|
file | diff | annotate |
Sat, 27 Apr 2013 20:50:20 +0200 |
uniform Proof.context for hyp_subst_tac;
|
file | diff | annotate |
Wed, 24 Apr 2013 17:47:22 +0200 |
renamed "set_natural" to "set_map", reflecting {Bl,Po,Tr} concensus
|
file | diff | annotate |
Thu, 18 Apr 2013 17:07:01 +0200 |
simplifier uses proper Proof.context instead of historic type simpset;
|
file | diff | annotate |
Tue, 02 Oct 2012 01:00:18 +0200 |
continued changing type of corec type
|
file | diff | annotate |
Tue, 02 Oct 2012 01:00:18 +0200 |
made (co)rec tactic more robust when the simplifier succeeds early
|
file | diff | annotate |
Mon, 01 Oct 2012 11:04:30 +0200 |
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 |
tweaked corecursor/coiterator tactic
|
file | diff | annotate |
Mon, 01 Oct 2012 10:34:58 +0200 |
changed the type of the recursor for nested recursion
|
file | diff | annotate |
Sun, 30 Sep 2012 22:02:34 +0200 |
tuning
|
file | diff | annotate |
Sun, 30 Sep 2012 12:04:13 +0200 |
tuned tactic
|
file | diff | annotate |
Fri, 28 Sep 2012 15:23:32 +0200 |
simplified simpset
|
file | diff | annotate |
Fri, 28 Sep 2012 15:14:11 +0200 |
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 |
tuned tactic
|
file | diff | annotate |
Fri, 28 Sep 2012 09:38:07 +0200 |
tuned tactic
|
file | diff | annotate |
Fri, 28 Sep 2012 09:12:50 +0200 |
renamed ML file in preparation for next step
|
file | diff | annotate | base |