Mercurial Mercurial > repos > isabelle / file revisions
summary | shortlog | changelog | graph | tags | bookmarks | branches | file | revisions | annotate | diff | comparison | rss | help
(0) -100 -60 tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML
Thu, 10 Mar 2016 19:15:06 +0100 blanchet don't throw an exception when trying to print an error message file | diff | annotate
Thu, 10 Mar 2016 18:32:12 +0100 blanchet eta-expansion done right in "primcorec" file | diff | annotate
Wed, 02 Mar 2016 10:02:12 +0100 traytel respect qualification when noting theorems in prim(co)rec file | diff | annotate
Mon, 15 Feb 2016 12:47:35 +0100 blanchet clearer error message file | diff | annotate
Sun, 13 Dec 2015 21:56:15 +0100 wenzelm more general types Proof.method / context_tactic; file | diff | annotate
Tue, 01 Dec 2015 13:07:40 +0100 blanchet tuned whitespace file | diff | annotate
Tue, 13 Oct 2015 09:21:15 +0200 haftmann prod_case as canonical name for product type eliminator file | diff | annotate
Wed, 07 Oct 2015 10:02:43 +0200 blanchet disable generation of 'case_transfer' for 'nibble', due to quadratic proof -- to make 'HOL-Proofs' happier file | diff | annotate
Tue, 06 Oct 2015 12:01:07 +0200 traytel collect the names from goals in favor of fragile exports file | diff | annotate
Thu, 01 Oct 2015 17:32:07 +0200 blanchet export '_cmd' functions file | diff | annotate
Fri, 25 Sep 2015 23:01:31 +0200 traytel more canonical context threading file | diff | annotate
Sun, 06 Sep 2015 22:14:51 +0200 haftmann prefer "uncurry" as canonical name for case distinction on products in combinatorial view file | diff | annotate
Thu, 16 Jul 2015 18:36:16 +0200 blanchet made code less loopy file | diff | annotate
Thu, 16 Jul 2015 17:38:36 +0200 blanchet generalized generic translation function file | diff | annotate
Mon, 13 Jul 2015 19:22:55 +0200 blanchet tuning file | diff | annotate
Thu, 09 Jul 2015 21:59:16 +0200 blanchet tuned ML signature (and rationalized code a bit) file | diff | annotate
Tue, 07 Jul 2015 18:37:25 +0200 blanchet tuned ML signature file | diff | annotate
Tue, 02 Jun 2015 11:03:02 +0200 wenzelm clarified context; file | diff | annotate
Fri, 10 Apr 2015 18:23:01 +0200 blanchet renamed ML funs file | diff | annotate
Fri, 10 Apr 2015 14:03:18 +0200 blanchet generalized code file | diff | annotate
Thu, 09 Apr 2015 18:46:16 +0200 blanchet tuned signature file | diff | annotate
Tue, 07 Apr 2015 17:24:55 +0200 blanchet generalized slightly file | diff | annotate
Tue, 07 Apr 2015 15:14:14 +0200 blanchet generalized code file | diff | annotate
Tue, 07 Apr 2015 15:14:12 +0200 blanchet generalized code file | diff | annotate
Tue, 07 Apr 2015 14:38:20 +0200 blanchet export ML function file | diff | annotate
Mon, 06 Apr 2015 17:06:48 +0200 wenzelm @{command_spec} is superseded by @{command_keyword}; file | diff | annotate
Wed, 01 Apr 2015 19:17:41 +0200 blanchet simplified code file | diff | annotate
Tue, 31 Mar 2015 00:11:54 +0200 wenzelm tuned signature; file | diff | annotate
Tue, 24 Mar 2015 23:39:42 +0100 wenzelm merged file | diff | annotate
Tue, 24 Mar 2015 18:36:29 +0100 wenzelm clarified role of Name.uu_, which happens to be the internal replacement of the first underscore under certain assumptions about the context; file | diff | annotate
Tue, 24 Mar 2015 18:10:56 +0100 blanchet tuning file | diff | annotate
Tue, 10 Mar 2015 21:31:19 +0100 blanchet export more functions (for future 'corec') file | diff | annotate
Tue, 10 Mar 2015 20:53:16 +0100 blanchet tuning file | diff | annotate
Tue, 10 Mar 2015 09:49:16 +0100 blanchet tuning file | diff | annotate
Thu, 05 Mar 2015 16:45:24 +0100 blanchet avoid needless 'if ... undefined' in generated theorems file | diff | annotate
Thu, 05 Mar 2015 14:25:45 +0100 blanchet deal better with corecursion through functions file | diff | annotate
Thu, 05 Mar 2015 13:44:41 +0100 blanchet removed too strict checks file | diff | annotate
Thu, 05 Mar 2015 12:32:11 +0100 blanchet message tuning file | diff | annotate
Thu, 05 Mar 2015 12:19:05 +0100 blanchet tuning file | diff | annotate
Thu, 05 Mar 2015 11:57:34 +0100 blanchet improved primcorec messages file | diff | annotate
Thu, 05 Mar 2015 11:57:34 +0100 blanchet improved primcorec messages file | diff | annotate
Thu, 05 Mar 2015 11:57:34 +0100 blanchet better primcorec messages file | diff | annotate
Thu, 05 Mar 2015 11:57:34 +0100 blanchet more primcorec messages file | diff | annotate
Thu, 05 Mar 2015 11:57:34 +0100 blanchet more precise primcorec messages file | diff | annotate
Thu, 05 Mar 2015 11:57:34 +0100 blanchet more precise primcorec messages file | diff | annotate
Thu, 05 Mar 2015 11:57:34 +0100 blanchet better primcorec messages file | diff | annotate
Thu, 05 Mar 2015 11:57:34 +0100 blanchet more 'primcorec' error handling file | diff | annotate
Thu, 05 Mar 2015 11:57:34 +0100 blanchet helpful error message when 'auto' fails file | diff | annotate
Thu, 05 Mar 2015 11:57:34 +0100 blanchet no quick_and_dirty for goals that may fail + tuned messages file | diff | annotate
Thu, 05 Mar 2015 11:57:34 +0100 blanchet tuned new primrec messages file | diff | annotate
Thu, 05 Mar 2015 11:57:34 +0100 blanchet reworked primcorec error messages file | diff | annotate
Wed, 04 Mar 2015 19:53:18 +0100 wenzelm tuned signature -- prefer qualified names; file | diff | annotate
Mon, 05 Jan 2015 21:24:14 +0100 blanchet generate [code] only with 'code' plugin enabled file | diff | annotate
Mon, 05 Jan 2015 10:09:42 +0100 blanchet added plugins syntax to prim(co)rec file | diff | annotate
Mon, 05 Jan 2015 09:54:41 +0100 blanchet tuning file | diff | annotate
Mon, 05 Jan 2015 06:56:15 +0100 blanchet tuning file | diff | annotate
Fri, 19 Dec 2014 14:06:13 +0100 desharna Add plugin to generate transfer theorem for primrec and primcorec file | diff | annotate
Wed, 26 Nov 2014 20:05:34 +0100 wenzelm renamed "pairself" to "apply2", in accordance to @{apply 2}; file | diff | annotate
Mon, 24 Nov 2014 12:35:13 +0100 blanchet tuned whitespace file | diff | annotate
Mon, 24 Nov 2014 12:35:13 +0100 blanchet keep all 'ctr' theorems file | diff | annotate
less more (0) -100 -60 tip
isabelle