Mercurial Mercurial > repos > isabelle / file revisions
summary | shortlog | changelog | graph | tags | bookmarks | branches | file | revisions | annotate | diff | comparison | rss | help
(0) tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/BNF/bnf_fp_util.ML
Mon, 06 Oct 2014 13:38:40 +0200 desharna rename 'dtor_set_induct_thms' to 'dtor_set_inducts' file | diff | annotate
Mon, 06 Oct 2014 13:38:13 +0200 desharna rename 'rel_xtor_co_induct_thm' to 'xtor_rel_co_induct' file | diff | annotate
Mon, 06 Oct 2014 13:37:38 +0200 desharna rename 'xtor_co_rec_o_map_thms' to 'xtor_co_rec_o_maps' 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
Thu, 25 Sep 2014 16:35:51 +0200 desharna generate 'dtor_corec_transfer' for codatatypes file | diff | annotate
Thu, 25 Sep 2014 16:35:50 +0200 desharna generate 'ctor_rec_transfer' for datatypes file | diff | annotate
Mon, 01 Sep 2014 14:14:47 +0200 traytel goal generation for xtor_co_rec_transfer file | diff | annotate
Thu, 25 Sep 2014 09:01:14 +0200 traytel even more deads go to the end (continuation of e3a01b73579f) file | diff | annotate
Sat, 13 Sep 2014 18:08:38 +0200 blanchet imported patch phantoms 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 generalized 'datatype' LaTeX antiquotation and added 'codatatype' file | diff | annotate
Mon, 08 Sep 2014 14:03:01 +0200 blanchet tuning file | diff | annotate
Thu, 04 Sep 2014 09:02:43 +0200 blanchet moved code around 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 made transfer functions slightly more general file | diff | annotate
Mon, 18 Aug 2014 17:19:58 +0200 blanchet reordered some (co)datatype property names for more consistency file | diff | annotate
Wed, 30 Jul 2014 10:50:28 +0200 desharna generate 'set_induct' theorem for codatatypes file | diff | annotate
Fri, 25 Jul 2014 11:26:10 +0200 blanchet tuning file | diff | annotate
Wed, 16 Jul 2014 10:13:00 +0200 desharna generate 'rel_sel' theorem for (co)datatypes file | diff | annotate
Mon, 07 Jul 2014 16:06:46 +0200 desharna refactor some tactics file | diff | annotate
Mon, 07 Jul 2014 16:06:46 +0200 desharna generate 'rel_cases' theorem for (co)datatypes file | diff | annotate
Thu, 03 Jul 2014 11:30:02 +0200 desharna generate 'rel_intros' theorem for (co)datatypes file | diff | annotate
Wed, 02 Jul 2014 17:01:49 +0200 desharna generate 'corec_code' theorem for codatatypes file | diff | annotate
Fri, 27 Jun 2014 10:11:44 +0200 blanchet tuned variable names file | diff | annotate
Wed, 23 Apr 2014 10:23:27 +0200 blanchet no need to make 'size' generation an interpretation -- overkill file | diff | annotate
Thu, 13 Mar 2014 11:15:04 +0100 traytel simplified internal codatatype construction file | diff | annotate
Fri, 07 Mar 2014 22:30:58 +0100 wenzelm more antiquotations; file | diff | annotate
Fri, 07 Mar 2014 14:21:15 +0100 blanchet use balanced tuples in 'primcorec' file | diff | annotate
Fri, 07 Mar 2014 14:21:15 +0100 blanchet tuning file | diff | annotate
Fri, 07 Mar 2014 01:02:21 +0100 blanchet balance tuples that represent curried functions file | diff | annotate
Thu, 06 Mar 2014 15:40:33 +0100 blanchet renamed 'fun_rel' to 'rel_fun' file | diff | annotate
Thu, 06 Mar 2014 13:36:48 +0100 blanchet renamed 'map_pair' to 'map_prod' file | diff | annotate
Thu, 06 Mar 2014 13:36:15 +0100 blanchet renamed 'map_sum' to 'sum_map' file | diff | annotate
Tue, 04 Mar 2014 18:57:17 +0100 blanchet more caching in composition pipeline file | diff | annotate
Tue, 04 Mar 2014 18:57:17 +0100 blanchet renamed a pair of low-level theorems to have c/dtor in their names (like the others) file | diff | annotate
Tue, 04 Mar 2014 12:32:33 +0100 traytel N2M does not use the low-level 'fold'; removed the latter from the fp_result interface; file | diff | annotate
Mon, 03 Mar 2014 12:48:20 +0100 blanchet rationalized internals file | diff | annotate
Mon, 03 Mar 2014 12:48:20 +0100 blanchet rationalized internals file | diff | annotate
Mon, 03 Mar 2014 12:48:20 +0100 blanchet got rid of automatically generated fold constant and theorems (to reduce overhead) file | diff | annotate
Mon, 03 Mar 2014 12:48:19 +0100 blanchet optimize cardinal bounds involving natLeq (omega) file | diff | annotate
Fri, 28 Feb 2014 17:54:52 +0100 traytel load Metis a little later file | diff | annotate
Tue, 25 Feb 2014 18:14:26 +0100 traytel joint work with blanchet: intermediate typedef for the input to fp-operations file | diff | annotate
Mon, 24 Feb 2014 00:04:48 +0100 blanchet added BNF cache (within one definition) file | diff | annotate
Sun, 23 Feb 2014 22:51:11 +0100 blanchet optimization of 'bnf_of_typ' if all variables are dead file | diff | annotate
Sun, 23 Feb 2014 22:51:11 +0100 blanchet added explicit killing file | diff | annotate
Fri, 21 Feb 2014 00:09:56 +0100 blanchet adapted to renaming of datatype 'cases' and 'recs' to 'case' and 'rec' file | diff | annotate
Wed, 19 Feb 2014 08:34:33 +0100 blanchet moved 'primrec' up (for real this time) and removed temporary 'old_primrec' file | diff | annotate
Tue, 18 Feb 2014 23:08:58 +0100 blanchet tuning file | diff | annotate
Fri, 14 Feb 2014 18:42:43 +0100 blanchet generate proper 'DtRec' indices in 'datatype_new_compat' for the case where some types are duplicated file | diff | annotate
Fri, 14 Feb 2014 17:18:28 +0100 blanchet better handling of recursion through functions file | diff | annotate
Wed, 12 Feb 2014 08:35:57 +0100 blanchet renamed '{prod,sum,bool,unit}_case' to 'case_...' file | diff | annotate
Wed, 12 Feb 2014 08:35:56 +0100 blanchet more liberal merging of BNFs and constructor sugar file | diff | annotate
Mon, 20 Jan 2014 18:24:56 +0100 blanchet tuned names file | diff | annotate
Mon, 20 Jan 2014 18:24:56 +0100 blanchet adjusted comments file | diff | annotate
Mon, 20 Jan 2014 18:24:56 +0100 blanchet avoid nested 'Tools' directories file | diff | annotate | base
less more (0) tip
isabelle