| Mon, 04 May 2015 20:05:50 +0200 |
wenzelm |
more on Isabelle document preparation and bibtex files;
|
changeset |
files
|
| Mon, 04 May 2015 19:55:30 +0200 |
wenzelm |
tuned spelling;
|
changeset |
files
|
| Sun, 03 May 2015 23:41:24 +0200 |
wenzelm |
updated screenshot;
|
changeset |
files
|
| Sun, 03 May 2015 22:15:29 +0200 |
blanchet |
improved one-line preplaying (don't rely on 'using x by simp' to mean 'by (simp add: x)' and beware of inaccessible '(local.)this')
|
changeset |
files
|
| Sun, 03 May 2015 18:14:11 +0200 |
blanchet |
made split-rule tactic go beyond constructors with 20 arguments
|
changeset |
files
|
| Sun, 03 May 2015 20:21:25 +0200 |
wenzelm |
proper fold painter according to jEdit options, not the hardwired default of JEditEmbeddedTextArea;
|
changeset |
files
|
| Sun, 03 May 2015 20:04:38 +0200 |
wenzelm |
tuned output to resemble input syntax more closely;
|
changeset |
files
|
| Sun, 03 May 2015 18:51:26 +0200 |
wenzelm |
updated Eisbach, using version fb741500f533 of its Bitbucket repository;
|
changeset |
files
|
| Sun, 03 May 2015 18:45:58 +0200 |
wenzelm |
proper header;
|
changeset |
files
|
| Sun, 03 May 2015 18:13:15 +0200 |
wenzelm |
tuned output;
|
changeset |
files
|
| Sun, 03 May 2015 17:52:27 +0200 |
wenzelm |
tuned output;
|
changeset |
files
|
| Sun, 03 May 2015 17:41:54 +0200 |
wenzelm |
tuned output;
|
changeset |
files
|
| Sun, 03 May 2015 17:36:46 +0200 |
wenzelm |
tuned output;
|
changeset |
files
|
| Sun, 03 May 2015 17:19:27 +0200 |
wenzelm |
tuned output -- avoid empty quites and extra breaks;
|
changeset |
files
|
| Sun, 03 May 2015 16:45:07 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| 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
|
| Fri, 01 May 2015 14:35:13 +0200 |
wenzelm |
clarified markup range;
|
changeset |
files
|
| Fri, 01 May 2015 13:58:06 +0200 |
wenzelm |
modifier markup for all parsed tokens;
|
changeset |
files
|
| Fri, 01 May 2015 00:27:04 +0200 |
wenzelm |
updated screenshots;
|
changeset |
files
|
| Thu, 30 Apr 2015 17:02:57 +0200 |
wenzelm |
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
|
changeset |
files
|
| Thu, 30 Apr 2015 17:00:50 +0200 |
wenzelm |
avoid potential conflict with Eisbach keyword (although keywords are local to the theory context);
|
changeset |
files
|
| Tue, 28 Apr 2015 13:30:28 +0200 |
blanchet |
allow sorts on dead variables in BNFs
|
changeset |
files
|
| Tue, 28 Apr 2015 11:48:44 +0200 |
wenzelm |
tuned whitespace;
|
changeset |
files
|
| Tue, 28 Apr 2015 11:47:49 +0200 |
wenzelm |
avoid auto-load dialog while exit/closeAllBuffers is active: the perspective manager happens to indicate this precisely in jEdit 5.2.0;
|
changeset |
files
|
| Mon, 27 Apr 2015 16:46:52 +0200 |
wenzelm |
code equations as displayable content in code dependency graph
|
changeset |
files
|
| Mon, 27 Apr 2015 15:53:11 +0200 |
wenzelm |
filtering of reflexive dependencies avoids problems with state-of-the-art graph browser;
|
changeset |
files
|
| Sat, 25 Apr 2015 20:49:26 +0200 |
wenzelm |
added checkbox for try0;
|
changeset |
files
|
| Sat, 25 Apr 2015 09:48:06 +0200 |
blanchet |
made CVC4 support work also without unsat cores
|
changeset |
files
|
| Fri, 24 Apr 2015 23:05:33 +0200 |
wenzelm |
more paranoia settings, e.g. relevant for Ubuntu 15.04;
|
changeset |
files
|
| Fri, 24 Apr 2015 22:30:56 +0200 |
wenzelm |
Added tag Isabelle2015-RC2 for changeset 8483c2883c8c
|
changeset |
files
|
| Fri, 24 Apr 2015 20:33:10 +0200 |
wenzelm |
always traverse required nodes, e.g. relevant for inlined errors of imported theory header;
|
changeset |
files
|
| Fri, 24 Apr 2015 19:08:43 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 24 Apr 2015 16:12:20 +0200 |
wenzelm |
tuned message, in accordance to ML side;
|
changeset |
files
|