Mercurial Mercurial > repos > isabelle / file revisions
summary | shortlog | changelog | graph | tags | bookmarks | branches | file | revisions | annotate | diff | comparison | rss | help
(0) -100 -60 tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
Mon, 06 Oct 2014 13:33:15 +0200 desharna add 'rel_intros' to 'fp_sugar' file | diff | annotate
Mon, 06 Oct 2014 13:33:04 +0200 desharna add 'rel_sels' to 'fp_sugar' file | diff | annotate
Mon, 06 Oct 2014 13:32:53 +0200 desharna add 'map_sels' to 'fp_sugar' file | diff | annotate
Mon, 06 Oct 2014 13:32:41 +0200 desharna add 'map_disc_iffs' to 'fp_sugar' file | diff | annotate
Thu, 02 Oct 2014 12:02:27 +0200 blanchet tuning file | diff | annotate
Mon, 29 Sep 2014 10:39:39 +0200 blanchet tuning file | diff | annotate
Fri, 26 Sep 2014 14:43:28 +0200 desharna refactor fp_sugar move theorems file | diff | annotate
Fri, 26 Sep 2014 14:43:26 +0200 desharna refactor fp_sugar move theorems file | diff | annotate
Fri, 26 Sep 2014 14:41:54 +0200 desharna refactor fp_sugar move theorems file | diff | annotate
Fri, 26 Sep 2014 14:41:15 +0200 desharna refactor fp_sugar move theorems file | diff | annotate
Fri, 26 Sep 2014 14:41:08 +0200 desharna refactor fp_sugar move theorems file | diff | annotate
Fri, 26 Sep 2014 14:36:54 +0200 desharna refactor fp_sugar with empty substructures file | diff | annotate
Fri, 26 Sep 2014 14:35:09 +0200 desharna add attribute 'case_names' to 'set_case' file | diff | annotate
Thu, 25 Sep 2014 16:35:56 +0200 desharna generate 'corec_transfer' for codatatypes file | diff | annotate
Thu, 25 Sep 2014 16:35:53 +0200 desharna generate 'rec_transfer' for datatypes file | diff | annotate
Wed, 24 Sep 2014 21:00:07 +0200 blanchet avoid type variable name clash file | diff | annotate
Wed, 24 Sep 2014 21:00:07 +0200 blanchet tuning file | diff | annotate
Tue, 16 Sep 2014 19:23:37 +0200 blanchet register 'prod' and 'sum' as datatypes, to allow N2M through them file | diff | annotate
Mon, 15 Sep 2014 18:12:09 +0200 blanchet tuning file | diff | annotate
Mon, 15 Sep 2014 17:56:37 +0200 blanchet refactoring file | diff | annotate
Mon, 15 Sep 2014 16:34:05 +0200 blanchet tuning file | diff | annotate
Mon, 15 Sep 2014 11:17:44 +0200 blanchet tuning file | diff | annotate
Mon, 15 Sep 2014 10:49:07 +0200 blanchet generate 'code' attribute only if 'code' plugin is enabled file | diff | annotate
Sat, 13 Sep 2014 18:08:38 +0200 blanchet imported patch phantoms file | diff | annotate
Fri, 12 Sep 2014 13:50:55 +0200 desharna refactor repeated terms in a single variable file | diff | annotate
Fri, 12 Sep 2014 13:50:51 +0200 desharna make 'ctr_transfer' tactic more robust file | diff | annotate
Fri, 12 Sep 2014 13:48:15 +0200 desharna make 'rel_sel' and 'map_sel' tactics more robust file | diff | annotate
Tue, 09 Sep 2014 23:54:47 +0200 blanchet tuning file | diff | annotate
Tue, 09 Sep 2014 20:51:36 +0200 blanchet avoid duplicate case names file | diff | annotate
Tue, 09 Sep 2014 20:51:36 +0200 blanchet nicer case names in the N2M case, similar to those generated by the old package (e.g. 'Cons_tree' instead of just 'Cons') file | diff | annotate
Tue, 09 Sep 2014 20:51:36 +0200 blanchet preserve case names in '(co)induct' theorems generated by prim(co)rec' file | diff | annotate
Tue, 09 Sep 2014 20:51:36 +0200 blanchet set 'fundef_cong' attribute also for (co)datatypes with no live type variables file | diff | annotate
Tue, 09 Sep 2014 20:51:36 +0200 blanchet prevent infinite loop when type variables are of a non-'type' sort file | diff | annotate
Tue, 09 Sep 2014 20:51:36 +0200 blanchet tuned code file | diff | annotate
Mon, 08 Sep 2014 19:21:07 +0200 blanchet honour sorts in N2M file | diff | annotate
Mon, 08 Sep 2014 16:51:35 +0200 blanchet proper sort constraints in map and rel theorems file | diff | annotate
Mon, 08 Sep 2014 16:09:10 +0200 blanchet made code work also in the presence of deads file | diff | annotate
Mon, 08 Sep 2014 14:03:01 +0200 blanchet properly note theorems for split recursors file | diff | annotate
Mon, 08 Sep 2014 14:03:01 +0200 blanchet extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions file | diff | annotate
Mon, 08 Sep 2014 14:03:01 +0200 blanchet tuning file | diff | annotate
Mon, 08 Sep 2014 14:03:01 +0200 blanchet export one more ML function file | diff | annotate
Mon, 08 Sep 2014 14:03:01 +0200 blanchet tuning file | diff | annotate
Fri, 05 Sep 2014 00:41:01 +0200 blanchet pretend code generation is a ctr_sugar plugin file | diff | annotate
Fri, 05 Sep 2014 00:41:01 +0200 blanchet added 'plugins' option to control which hooks are enabled file | diff | annotate
Fri, 05 Sep 2014 00:41:01 +0200 blanchet introduced mechanism to filter interpretations file | diff | annotate
Fri, 05 Sep 2014 00:41:01 +0200 blanchet fixed infinite loops in 'register' functions + more uniform API file | diff | annotate
Fri, 05 Sep 2014 00:41:01 +0200 blanchet named interpretations file | diff | annotate
Fri, 05 Sep 2014 00:41:00 +0200 blanchet centralized and cleaned up naming handling file | diff | annotate
Thu, 04 Sep 2014 11:20:59 +0200 blanchet tweaked setup for datatype realizer file | diff | annotate
Thu, 04 Sep 2014 09:02:43 +0200 blanchet moved code around file | diff | annotate
Thu, 04 Sep 2014 09:02:43 +0200 blanchet tuned size function generation file | diff | annotate
Wed, 03 Sep 2014 22:49:05 +0200 blanchet introduced local interpretation mechanism for BNFs, to solve issues with datatypes in locales file | diff | annotate
Wed, 03 Sep 2014 22:47:35 +0200 blanchet tuned BNF database handling file | diff | annotate
Wed, 03 Sep 2014 00:31:37 +0200 blanchet tuning file | diff | annotate
Mon, 01 Sep 2014 16:17:47 +0200 blanchet more compatibility between old- and new-style datatypes file | diff | annotate
Mon, 01 Sep 2014 16:17:47 +0200 blanchet added theory-based getters for convenience file | diff | annotate
Mon, 01 Sep 2014 16:17:47 +0200 blanchet made transfer functions slightly more general file | diff | annotate
Mon, 01 Sep 2014 16:17:46 +0200 blanchet renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place file | diff | annotate
Mon, 01 Sep 2014 13:23:39 +0200 desharna generate 'rel_transfer' for BNFs file | diff | annotate
Fri, 29 Aug 2014 14:36:51 +0200 desharna generate 'disc_transfer' for (co)datatypes file | diff | annotate
less more (0) -100 -60 tip
isabelle