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.ML
Fri, 18 Oct 2013 16:02:07 +0200 blanchet tuning file | diff | annotate
Fri, 18 Oct 2013 15:25:39 +0200 blanchet conceal more ugly constructions file | diff | annotate
Fri, 18 Oct 2013 15:19:21 +0200 blanchet conceal prim(co)rec definitions file | diff | annotate
Fri, 18 Oct 2013 15:12:04 +0200 blanchet avoid 'co_' prefix with underscore meaning 'co', since it is our only possible identifier representation of '(co)' file | diff | annotate
Fri, 18 Oct 2013 10:35:56 +0200 blanchet make sure that registered code equations are actually equations file | diff | annotate
Thu, 17 Oct 2013 10:29:28 +0200 blanchet graceful handling of abort file | diff | annotate
Thu, 17 Oct 2013 10:06:48 +0200 panny generalized interface file | diff | annotate
Wed, 16 Oct 2013 20:44:33 +0200 panny use Code.abort instead of undefined in auto-generated equations file | diff | annotate
Mon, 14 Oct 2013 10:55:49 +0200 blanchet keep temporary error handling in there until code equations are properly generated file | diff | annotate
Mon, 14 Oct 2013 09:31:42 +0200 blanchet tuned names file | diff | annotate
Mon, 14 Oct 2013 09:17:04 +0200 blanchet strengthened tactic w.r.t. "let" file | diff | annotate
Fri, 11 Oct 2013 23:15:30 +0200 panny compile -- fix typo introduced in 07a8145aaeba 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: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
Fri, 04 Oct 2013 18:27:07 +0200 panny process code-style inputs file | diff | annotate
Wed, 02 Oct 2013 22:54:42 +0200 blanchet strengthened tactic (primcorec_sel_tac) + tuning file | diff | annotate
Wed, 02 Oct 2013 16:29:40 +0200 blanchet don't register equations of the form 'f x = ...' as simp rules, even if they are safe (noncorecursive), because they unfold too aggresively concepts users are likely to want to stay folded file | diff | annotate
Wed, 02 Oct 2013 15:13:41 +0200 traytel made SML/NJ happy file | diff | annotate
Tue, 01 Oct 2013 17:04:27 +0200 traytel improved backwards compatiblity of primrec_new (Isabelle/ML interface, attributes, etc.) file | diff | annotate
Mon, 30 Sep 2013 22:36:43 +0200 blanchet made SML/NJ happy file | diff | annotate
Mon, 30 Sep 2013 18:08:35 +0200 blanchet made SML/NJ happy file | diff | annotate
Mon, 30 Sep 2013 17:53:44 +0200 blanchet made SML/NJ happier file | diff | annotate
Thu, 26 Sep 2013 16:25:12 +0200 blanchet tuning file | diff | annotate
Thu, 26 Sep 2013 16:10:57 +0200 blanchet tuning 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:57:39 +0200 blanchet strengthen tactic file | diff | annotate
Thu, 26 Sep 2013 10:26:00 +0200 blanchet use needed case theorems file | diff | annotate
Thu, 26 Sep 2013 02:09:52 +0200 blanchet more powerful/robust tactics file | diff | annotate
Thu, 26 Sep 2013 01:05:07 +0200 blanchet tuning file | diff | annotate
Thu, 26 Sep 2013 01:05:06 +0200 blanchet made tactic more flexible w.r.t. case expressions and such file | diff | annotate
Wed, 25 Sep 2013 21:25:53 +0200 panny simplified code 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 14:21:18 +0200 blanchet move useful functions to library file | diff | annotate
Wed, 25 Sep 2013 13:39:34 +0200 panny merge file | diff | annotate
Wed, 25 Sep 2013 12:43:20 +0200 panny simplified code file | diff | annotate
Wed, 25 Sep 2013 00:38:13 +0200 panny add non-corecursive constructor view theorems to simps file | diff | annotate
Wed, 25 Sep 2013 12:29:06 +0200 blanchet more powerful fold file | diff | annotate
Tue, 24 Sep 2013 22:21:51 +0200 blanchet commented out debugging output in "primcorec" 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 18:07:09 +0200 panny support "of" syntax to disambiguate selector equations file | diff | annotate
Tue, 24 Sep 2013 17:54:09 +0200 blanchet don't note more induction principles than there are functions + tuning file | diff | annotate
Tue, 24 Sep 2013 15:16:59 +0200 panny add "primcorec" command (cf. ae7f50e70c09) file | diff | annotate
Tue, 24 Sep 2013 00:18:22 +0200 blanchet set code and nitpick_simp attributes on primcorec theorems file | diff | annotate
Mon, 23 Sep 2013 10:58:37 +0200 blanchet note coinduct theorems in "primcorec" file | diff | annotate
Mon, 23 Sep 2013 10:45:26 +0200 blanchet generate "simps" from "primcorec" file | diff | annotate
Mon, 23 Sep 2013 10:38:23 +0200 blanchet undid copy-paste file | diff | annotate
Mon, 23 Sep 2013 10:34:10 +0200 blanchet avoid giving same name to simplifying constructor as to real one (to avoid risks of confusion when reading the code) file | diff | annotate
Mon, 23 Sep 2013 10:30:43 +0200 blanchet tuned code file | diff | annotate
Fri, 20 Sep 2013 16:32:27 +0200 blanchet renamed "primcorec" to "primcorecursive", to open the door to a 'theory -> theory' command called "primcorec" (cf. "fun" vs. "function") file | diff | annotate
Fri, 20 Sep 2013 00:08:42 +0200 blanchet setting the stage for safe constructor simp rules file | diff | annotate
Thu, 19 Sep 2013 23:54:54 +0200 blanchet added TODO file | diff | annotate
Thu, 19 Sep 2013 17:38:03 +0200 traytel don't declare ctr view primcorec theorems as simp (they loop) file | diff | annotate
Thu, 19 Sep 2013 16:12:43 +0200 panny simplified code; eliminated some dummyTs 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:32 +0200 blanchet generalize code to handle zero-argument case gracefully (e.g. for nullay functions defined over codatatypes that corecurse through "fun" file | diff | annotate
Thu, 19 Sep 2013 01:09:25 +0200 blanchet simplified code file | diff | annotate
less more (0) -60 tip
isabelle