| Sat, 02 May 2015 13:58:06 +0200 |
kuncar |
equivalence in code_dt data structure must respect both rty and qty
|
changeset |
files
|
| Sat, 02 May 2015 13:58:06 +0200 |
kuncar |
don't use the human-readable version of the rsp thm as a goal in the ML interface (there is no formal definition of its statement); make tactics more robust wrt. predicates in predicators; tuned
|
changeset |
files
|
| 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
|
| Tue, 18 Nov 2014 16:19:57 +0100 |
kuncar |
useful function
|
changeset |
files
|
| Tue, 18 Nov 2014 16:19:57 +0100 |
kuncar |
parametrize liting of terms by quotients
|
changeset |
files
|
| Tue, 18 Nov 2014 16:19:57 +0100 |
kuncar |
improve handling of predicators in rsp_thm
|
changeset |
files
|