Mercurial Mercurial > repos > isabelle / file revisions
summary | shortlog | changelog | graph | tags | bookmarks | branches | file | revisions | annotate | diff | comparison | rss | help
(0) -60 tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Codatatype/Tools/bnf_fp_sugar.ML
Fri, 14 Sep 2012 12:09:27 +0200 blanchet tuning file | diff | annotate
Fri, 14 Sep 2012 12:09:27 +0200 blanchet renamed "mk_UnN" to "mk_UnIN" 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
Fri, 14 Sep 2012 12:09:27 +0200 blanchet derive induction via backward proof, to ensure that the premises are in the right order for constructors like "X x y x" where x and y are mutually recursive file | diff | annotate
Wed, 12 Sep 2012 23:06:39 +0200 blanchet rough and ready induction file | diff | annotate
Wed, 12 Sep 2012 17:26:05 +0200 blanchet tuning file | diff | annotate
Wed, 12 Sep 2012 17:26:05 +0200 blanchet set up things for (co)induction sugar file | diff | annotate
Wed, 12 Sep 2012 17:26:05 +0200 blanchet tuning file | diff | annotate
Wed, 12 Sep 2012 12:06:03 +0200 blanchet reuse generated names (they look better + slightly more efficient) file | diff | annotate
Wed, 12 Sep 2012 11:47:51 +0200 blanchet desambiguate grammar (e.g. for Nil's mixfix ("[]")) file | diff | annotate
Wed, 12 Sep 2012 06:27:36 +0200 blanchet tuning file | diff | annotate
Wed, 12 Sep 2012 05:03:18 +0200 blanchet reorganized dependencies so that the sugar does not depend on GFP -- this will be essential for bootstrapping file | diff | annotate
Wed, 12 Sep 2012 00:55:11 +0200 blanchet added optional qualifiers for constructors and destructors, similarly to the old package file | diff | annotate
Wed, 12 Sep 2012 00:20:37 +0200 blanchet added attributes to theorems file | diff | annotate
Tue, 11 Sep 2012 22:31:43 +0200 blanchet support for sort constraints in new (co)data commands file | diff | annotate
Tue, 11 Sep 2012 22:13:22 +0200 blanchet provide a programmatic interface for FP sugar file | diff | annotate
Tue, 11 Sep 2012 18:58:29 +0200 blanchet allow defaults for one datatype to involve the constructor of another one in the mutually recursive case file | diff | annotate
Tue, 11 Sep 2012 18:39:47 +0200 blanchet added "defaults" option file | diff | annotate
Tue, 11 Sep 2012 16:08:55 +0200 blanchet allow default values for selectors in low-level "wrap_data" command file | diff | annotate
Tue, 11 Sep 2012 14:51:52 +0200 blanchet added no_dests option file | diff | annotate
Tue, 11 Sep 2012 13:10:34 +0200 blanchet tuning 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:14 +0200 blanchet split sum types in corecursor definition 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
Tue, 11 Sep 2012 13:06:13 +0200 blanchet reverted "id" change: The problem is rather that the "%c. f c" argument sometimes gets eta-reduced file | diff | annotate
Tue, 11 Sep 2012 09:40:05 +0200 blanchet generate "id" rather than (%v. v) file | diff | annotate
Tue, 11 Sep 2012 09:40:05 +0200 blanchet correctly generate sel_coiter and sel_corec theorems file | diff | annotate
Mon, 10 Sep 2012 21:44:43 +0200 blanchet generate "sel_coiters" and friends 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 fixed base case of "mk_sumEN_balanced" file | diff | annotate
Mon, 10 Sep 2012 17:36:02 +0200 blanchet avoid type inference + tuning file | diff | annotate
Mon, 10 Sep 2012 17:35:53 +0200 blanchet use balanced sums for constructors (to gracefully handle 100 constructors or more) file | diff | annotate
Mon, 10 Sep 2012 17:32:39 +0200 blanchet busted -- let's use more neutral names file | diff | annotate
Sun, 09 Sep 2012 21:13:15 +0200 traytel full name of a type as key in bnf table 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 19:05:53 +0200 blanchet tuning 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:51:17 +0200 blanchet reactivated generation of "coiters" theorems 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:37:23 +0200 blanchet oops file | diff | annotate
Sat, 08 Sep 2012 21:21:27 +0200 blanchet fixed bug with one-value types with phantom type arguments file | diff | annotate
Sat, 08 Sep 2012 21:04:27 +0200 blanchet imported patch debugging 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 comment out code that's not ready file | diff | annotate
Sat, 08 Sep 2012 21:04:26 +0200 blanchet tuning file | diff | annotate
Sat, 08 Sep 2012 21:04:26 +0200 blanchet construct the right iterator theorem in the recursive case 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 more sugar on codatatypes 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 define coiterators file | diff | annotate
Sat, 08 Sep 2012 21:04:26 +0200 blanchet TODO file | diff | annotate
Sat, 08 Sep 2012 21:04:26 +0200 blanchet tuning 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
Sat, 08 Sep 2012 21:04:26 +0200 blanchet generate iter/rec goals file | diff | annotate
less more (0) -60 tip
isabelle