| Mon, 13 Apr 2015 15:27:34 +0200 | kuncar | go back to the complicated code equation registration (because of type classes) that was lost in 922586b1bc87; make it even more hackish to get which code equation was used | changeset | files |
| 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 | changeset | files |
| Fri, 05 Dec 2014 14:14:36 +0100 | kuncar | tuned proof; forget the transfer rule for size_fset | changeset | files |
| Fri, 05 Dec 2014 14:14:36 +0100 | kuncar | return also which code equation was used; tuned | changeset | files |
| Fri, 05 Dec 2014 14:14:36 +0100 | kuncar | publish lifting_forget and lifting_udpate interface | changeset | files |
| Fri, 05 Dec 2014 14:14:36 +0100 | kuncar | note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional | changeset | files |
| Tue, 18 Nov 2014 16:19:57 +0100 | kuncar | export the result of lifting_def | changeset | files |