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/BNF/Tools/bnf_fp_rec_sugar_util.ML
Mon, 11 Nov 2013 17:38:53 +0100 blanchet tuned signature file | diff | annotate
Mon, 04 Nov 2013 16:53:43 +0100 blanchet split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec') file | diff | annotate
Mon, 04 Nov 2013 14:46:38 +0100 blanchet more robust n2m w.r.t. 'let's file | diff | annotate
Mon, 04 Nov 2013 11:59:08 +0100 blanchet strengthened tactic file | diff | annotate
Mon, 04 Nov 2013 10:52:41 +0100 blanchet typo file | diff | annotate
Sat, 26 Oct 2013 12:54:57 +0200 blanchet align 'primrec_new' on 'primcorec' (+ got rid of one more 'dummyT') file | diff | annotate
Sat, 26 Oct 2013 12:54:39 +0200 blanchet convenience: handle composition gracefully in map in 'primcorec', analogously to 'primrec_new' file | diff | annotate
Thu, 24 Oct 2013 19:43:21 +0200 blanchet handle applied ctor arguments gracefully when computing 'callssss' (for recursion through functions) file | diff | annotate
Thu, 24 Oct 2013 18:37:54 +0200 blanchet more correct (!) types for recursive calls file | diff | annotate
Thu, 24 Oct 2013 15:56:03 +0200 blanchet watch out for 'case' constant canditates whose general type is 'a (e.g. 'undefined') file | diff | annotate
Mon, 21 Oct 2013 23:45:27 +0200 blanchet made lower-level function available file | diff | annotate
Sun, 20 Oct 2013 19:23:28 +0200 blanchet gracefully handle case where a nested recursive variable appears directly on the rhs of a primcorec equation file | diff | annotate
Fri, 18 Oct 2013 20:26:46 +0200 blanchet handle composition for multiple arguments correctly file | diff | annotate
Fri, 18 Oct 2013 18:58:46 +0200 blanchet set stage for more flexible 'primrec' syntax for recursion through functions file | diff | annotate
Thu, 17 Oct 2013 18:53:00 +0200 blanchet handle nested tuples in 'let's file | diff | annotate
Thu, 17 Oct 2013 13:37:13 +0200 blanchet also unfold let (_, _) = ... syntax file | diff | annotate
Thu, 17 Oct 2013 11:27:53 +0200 blanchet added helper function (that solves chicken-and-egg problem w.r.t. "callssss") file | diff | annotate
Mon, 14 Oct 2013 10:50:44 +0200 blanchet tuning (simplified parts of 92c5bd3b342d) file | diff | annotate
Mon, 14 Oct 2013 10:27:16 +0200 blanchet tuning file | diff | annotate
Mon, 14 Oct 2013 09:31:42 +0200 blanchet tuned names file | diff | annotate
Fri, 11 Oct 2013 20:47:37 +0200 panny pass the right theorems to tactic file | diff | annotate
Fri, 11 Oct 2013 16:31:23 +0200 panny prove user-supplied equations for ctr and code reductions, preserving "let"s, "case"s etc.; file | diff | annotate
Mon, 07 Oct 2013 23:38:57 +0200 blanchet allow 'let's around constructors in constructor view file | diff | annotate
Sun, 06 Oct 2013 20:54:28 +0200 blanchet strengthen the tactics to bring them in sync with the simplifications taking place in the code (and weaken the simplifications a bit -- let's not deal with implies) file | diff | annotate
Sun, 06 Oct 2013 20:24:06 +0200 blanchet generate optimized DNF formula file | diff | annotate
Sun, 06 Oct 2013 20:24:05 +0200 blanchet rationalized negation code file | diff | annotate
Tue, 01 Oct 2013 22:50:42 +0200 blanchet allow uncurried lambda-abstractions on rhs of "primcorec" file | diff | annotate
Tue, 01 Oct 2013 14:13:24 +0200 blanchet got rid of dead feature file | diff | annotate
Tue, 01 Oct 2013 14:05:25 +0200 blanchet renamed theory file file | diff | annotate
Sat, 28 Sep 2013 22:47:17 +0200 wenzelm make SML/NJ more happy; file | diff | annotate
Fri, 27 Sep 2013 19:30:49 +0200 blanchet faster exit in common case file | diff | annotate
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
less more (0) -60 tip
isabelle