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
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
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
less more (0) -60 tip
isabelle