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/BNF/Tools/bnf_fp_rec_sugar_util.ML
Thu, 26 Sep 2013 16:25:12 +0200 blanchet tuning file | diff | annotate
Thu, 26 Sep 2013 16:17:34 +0200 blanchet avoid calls to nth with ~1 file | diff | annotate
Thu, 26 Sep 2013 13:51:08 +0200 blanchet use new "sel_split(_asm)" to avoid giving rise to quantifiers, which would in turn require relying on injectivity file | diff | annotate
Thu, 26 Sep 2013 10:26:00 +0200 blanchet use needed case theorems file | diff | annotate
Wed, 25 Sep 2013 21:25:53 +0200 panny simplified code file | diff | annotate
Wed, 25 Sep 2013 18:49:37 +0200 blanchet don't generate wrong type file | diff | annotate
Wed, 25 Sep 2013 18:00:53 +0200 blanchet proper handling of abstractions file | diff | annotate
Wed, 25 Sep 2013 17:11:17 +0200 blanchet fixed off-by-one bug file | diff | annotate
Wed, 25 Sep 2013 17:01:29 +0200 blanchet further improved 'code' helper functions file | diff | annotate
Wed, 25 Sep 2013 16:57:48 +0200 blanchet removed spurious recursion file | diff | annotate
Wed, 25 Sep 2013 16:52:51 +0200 blanchet robustness file | diff | annotate
Wed, 25 Sep 2013 16:43:46 +0200 blanchet thread through bound types file | diff | annotate
Wed, 25 Sep 2013 16:43:46 +0200 blanchet killed redundant argument file | diff | annotate
Wed, 25 Sep 2013 16:43:46 +0200 blanchet improved massaging of case expressions file | diff | annotate
Wed, 25 Sep 2013 16:43:46 +0200 blanchet filled in gap in library offering file | diff | annotate
Wed, 25 Sep 2013 14:28:10 +0200 blanchet break more conjunctions file | diff | annotate
Wed, 25 Sep 2013 14:21:18 +0200 blanchet move useful functions to library file | diff | annotate
Wed, 25 Sep 2013 12:29:06 +0200 blanchet more powerful fold file | diff | annotate
Wed, 25 Sep 2013 12:00:22 +0200 blanchet properly fold over branches file | diff | annotate
Wed, 25 Sep 2013 10:53:09 +0200 blanchet removed dead code file | diff | annotate
Wed, 25 Sep 2013 10:45:12 +0200 blanchet keep a database of free constructor type information file | diff | annotate
Wed, 25 Sep 2013 10:26:04 +0200 blanchet generalized case-handling code a bit file | diff | annotate
Wed, 25 Sep 2013 10:17:18 +0200 blanchet support cases for new-style (co)datatypes file | diff | annotate
Wed, 25 Sep 2013 09:35:37 +0200 blanchet use case rather than sequence of ifs in expansion file | diff | annotate
Tue, 24 Sep 2013 20:40:36 +0200 blanchet started adding support for "nat_case" as case study for all "case" constructs file | diff | annotate
Tue, 24 Sep 2013 19:15:50 +0200 blanchet made SML/NJ happy file | diff | annotate
Tue, 24 Sep 2013 19:15:49 +0200 blanchet tuning file | diff | annotate
Fri, 20 Sep 2013 11:44:30 +0200 blanchet have "datatype_new_compat" register induction and recursion theorems in nested case file | diff | annotate
Thu, 19 Sep 2013 20:03:42 +0200 blanchet killed exceptional code that is anyway no longer needed, now that the 'simp' attribute has been taken away -- this solves issues in 'primcorec' file | diff | annotate
Thu, 19 Sep 2013 12:20:12 +0200 blanchet avoid infinite loop for unapplied terms + tuning file | diff | annotate
Thu, 19 Sep 2013 11:27:30 +0200 blanchet give lambda abstractions a chance, as an alternative to function composition, for corecursion via "fun" file | diff | annotate
Thu, 19 Sep 2013 03:29:33 +0200 blanchet added auxiliary function file | diff | annotate
Thu, 19 Sep 2013 02:30:45 +0200 blanchet added helper function for code equations in primcorec file | diff | annotate
Thu, 19 Sep 2013 01:09:25 +0200 blanchet split functionality into two functions to avoid redoing work over and over file | diff | annotate
Thu, 19 Sep 2013 01:09:25 +0200 blanchet added massaging function for primcorec code equations file | diff | annotate
Thu, 19 Sep 2013 01:09:25 +0200 blanchet simplified code file | diff | annotate
Thu, 19 Sep 2013 01:09:25 +0200 blanchet no need for beta-eta contraction file | diff | annotate
Thu, 19 Sep 2013 01:09:25 +0200 blanchet generalize helper function file | diff | annotate
Wed, 18 Sep 2013 20:43:55 +0200 blanchet enrich data structure file | diff | annotate
Fri, 13 Sep 2013 02:55:04 +0200 blanchet made non-co case more robust as well (cf. b6e2993fd0d3) file | diff | annotate
Fri, 13 Sep 2013 02:26:59 +0200 blanchet don't wrongly destroy sum types in coiterators file | diff | annotate
Fri, 13 Sep 2013 00:55:44 +0200 blanchet beware of multi-constructor datatypes (cf. 27c418b7b985) file | diff | annotate
Fri, 13 Sep 2013 00:39:24 +0200 blanchet beware of single-constructor datatypes, with no discriminators file | diff | annotate
Mon, 09 Sep 2013 14:22:11 +0200 blanchet include map theorems in datastructure for "primcorec" file | diff | annotate
Mon, 09 Sep 2013 13:47:58 +0200 blanchet enriched data structure with necessary theorems file | diff | annotate
Thu, 05 Sep 2013 01:58:48 +0200 panny support indirect corecursion file | diff | annotate
Fri, 30 Aug 2013 14:17:19 +0200 blanchet more canonical naming file | diff | annotate
Fri, 30 Aug 2013 11:27:23 +0200 blanchet moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository file | diff | annotate
less more (0) tip
isabelle