| Sun, 03 May 2015 16:44:38 +0200 |
wenzelm |
suppress formal sort-constraints, in accordance to norm_hhf_eqs;
|
changeset |
files
|
| Sun, 03 May 2015 14:35:48 +0200 |
wenzelm |
make SML/NJ more happy;
|
changeset |
files
|
| Sun, 03 May 2015 14:12:10 +0200 |
wenzelm |
tuned message;
|
changeset |
files
|
| Sat, 02 May 2015 13:58:06 +0200 |
kuncar |
add testing file for code_dt extension of lifting
|
changeset |
files
|
| Sat, 02 May 2015 13:58:06 +0200 |
kuncar |
handle error messages also in after_qed
|
changeset |
files
|
| Sat, 02 May 2015 13:58:06 +0200 |
kuncar |
reorder some steps in the construction to support mutual datatypes
|
changeset |
files
|
| Sat, 02 May 2015 13:58:06 +0200 |
kuncar |
more readable error message if some types do not correspond to sort constraints of the datatype
|
changeset |
files
|
| Sat, 02 May 2015 13:58:06 +0200 |
kuncar |
better precomputing
|
changeset |
files
|
| 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
|
| Tue, 18 Nov 2014 16:19:57 +0100 |
kuncar |
tuned; store pred_simps
|
changeset |
files
|
| Tue, 18 Nov 2014 16:19:57 +0100 |
kuncar |
lift_definition: return the result of lifting
|
changeset |
files
|
| Tue, 18 Nov 2014 16:19:57 +0100 |
kuncar |
lift_definition: interface also with tactic
|
changeset |
files
|
| Tue, 18 Nov 2014 16:19:57 +0100 |
kuncar |
generalize prove_schematic_quot_thm
|
changeset |
files
|
| Tue, 18 Nov 2014 16:19:51 +0100 |
kuncar |
added pred_def, rel_eq_onp tuned
|
changeset |
files
|
| Sun, 03 May 2015 00:01:10 +0200 |
wenzelm |
misc tuning, based on warnings by IntelliJ IDEA;
|
changeset |
files
|
| Fri, 01 May 2015 15:33:43 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 01 May 2015 15:18:50 +0200 |
wenzelm |
updated screenshot;
|
changeset |
files
|