| Mon, 24 Feb 2020 21:46:45 +0100 | traytel | lift BNF witnesses for quotients (unless better ones are specified by the user) | file | diff | annotate |
| Tue, 07 Jan 2020 14:58:01 +0100 | traytel | eliminated one redundant proof obligation in lift_bnf for quotients | file | diff | annotate |
| Tue, 10 Dec 2019 01:06:39 +0100 | traytel | an extensive example for lift_bnf across quotients | file | diff | annotate |