| Fri, 22 Jul 2022 14:39:56 +0200 | Fabian Huch | tuned (some HOL lints, by Yecine Megdiche); | file | diff | annotate |
| Mon, 11 May 2020 11:15:41 +0100 | paulson | the Uniq quantifier | file | diff | annotate |
| Sun, 05 Apr 2020 22:04:19 +0100 | paulson | fixed more nasty proofs | file | diff | annotate |
| Sun, 01 Dec 2019 08:00:59 +0000 | haftmann | characterization of singleton bit operation | file | diff | annotate |
| Wed, 23 Oct 2019 16:09:23 +0000 | haftmann | tuned syntax | file | diff | annotate |
| Thu, 08 Aug 2019 12:18:27 +0200 | wenzelm | prefer named lemmas -- more compact proofterms; | file | diff | annotate |
| Sun, 06 Jan 2019 15:04:34 +0100 | wenzelm | isabelle update -u path_cartouches; | file | diff | annotate |
| Fri, 04 Jan 2019 23:22:53 +0100 | wenzelm | isabelle update -u control_cartouches; | file | diff | annotate |
| Wed, 27 Jun 2018 10:18:03 +0200 | immler | added lemmas and transfer rules | file | diff | annotate |
| Wed, 10 Jan 2018 15:25:09 +0100 | nipkow | ran isabelle update_op on all sources | file | diff | annotate |
| Fri, 28 Oct 2016 19:54:41 +0200 | kuncar | a more general relator domain rule for the function type | file | diff | annotate |
| Mon, 03 Oct 2016 14:34:32 +0200 | haftmann | more lemmas | file | diff | annotate |
| Wed, 22 Jun 2016 10:09:20 +0200 | wenzelm | bundle lifting_syntax; | file | diff | annotate |
| Fri, 13 May 2016 20:24:10 +0200 | wenzelm | eliminated use of empty "assms"; | file | diff | annotate |
| Tue, 16 Feb 2016 22:28:19 +0100 | traytel | make predicator a first-class bnf citizen | file | diff | annotate |
| Wed, 11 Nov 2015 09:48:24 +0100 | Andreas Lochbihler | add various lemmas | file | diff | annotate |
| Sat, 18 Jul 2015 22:58:50 +0200 | wenzelm | isabelle update_cartouches; | file | diff | annotate |
| Fri, 05 Dec 2014 14:14:36 +0100 | kuncar | Workaround that allows us to execute lifted constants that have as a return type a datatype containing a subtype | file | diff | annotate |
| Wed, 11 Feb 2015 15:03:21 +0100 | Andreas Lochbihler | more transfer rules | file | diff | annotate |
| Wed, 11 Feb 2015 13:52:12 +0100 | Andreas Lochbihler | add parametricity rule for Ex1 | file | diff | annotate |
| Wed, 11 Feb 2015 13:51:16 +0100 | Andreas Lochbihler | add intro and elim rules for right_total | 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 |
| Mon, 15 Dec 2014 07:20:48 +0100 | blanchet | renamed theory file | file | diff | annotate |
| Fri, 07 Nov 2014 11:28:37 +0100 | traytel | more complete fp_sugars for sum and prod; | file | diff | annotate |
| Sun, 02 Nov 2014 18:21:45 +0100 | wenzelm | modernized header uniformly as section; | file | diff | annotate |
| Wed, 29 Oct 2014 15:02:29 +0100 | wenzelm | modernized setup; | file | diff | annotate |
| Thu, 25 Sep 2014 16:35:56 +0200 | desharna | generate 'corec_transfer' for codatatypes | file | diff | annotate |
| Thu, 25 Sep 2014 16:35:50 +0200 | desharna | generate 'ctor_rec_transfer' for datatypes | file | diff | annotate |
| Fri, 19 Sep 2014 10:40:56 +0200 | traytel | typo | file | diff | annotate |