2015-05-17 wenzelm 2015-05-17 added Eisbach manual, using version 8845c4cb28b6 of its Bitbucket repository;
2015-05-17 wenzelm 2015-05-17 updated Eisbach, using version 134bc592909c of its Bitbucket repository;
2015-05-17 wenzelm 2015-05-17 tuned;
2015-05-16 wenzelm 2015-05-16 updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
2015-05-13 wenzelm 2015-05-13 clarified alias: proper update of new accesses instead of conservative insert (via merge), otherwise "local.foo" could take precedence over "foo";
2015-05-13 wenzelm 2015-05-13 tuned whitespace;
2015-05-13 wenzelm 2015-05-13 more permissive operation: allow to print undeclared name space entries, e.g. print_simpset with "record" simproc;
2015-05-09 wenzelm 2015-05-09 Added tag Isabelle2015-RC4 for changeset 05fe9bdc4f8f
2015-05-09 blanchet 2015-05-09 new CVC4 component
2015-05-09 blanchet 2015-05-09 took out unreliable 'blast' from tactic altogether
2015-05-08 wenzelm 2015-05-08 clarified tooltip;
2015-05-08 wenzelm 2015-05-08 sledgehammer panel operation re-uses more of the Isar command, notably Try0.silence_methods to avoid spurious warnings intruding the document view;
2015-05-08 wenzelm 2015-05-08 more standard command setup;
2015-05-08 wenzelm 2015-05-08 silence local Unify.trace_bound as well: existing tools either refer to Proof.context or theory;
2015-05-08 wenzelm 2015-05-08 more conservative Document_Model.init: avoid Document.Node.Clear due to change of token marker (e.g. due to change of jEdit mode properties); clarified Isabelle.buffer_token_marker;
2015-05-07 wenzelm 2015-05-07 use display_graph_old for locale_deps, to show a bit more than nothing for cyclic graphs;
2015-05-07 wenzelm 2015-05-07 no GUI_Thread for SideKick parsers (in contrast to 4c8205fe3644), to avoid danger of deadlock due to nested context switch;
2015-05-06 wenzelm 2015-05-06 updated screenshot;
2015-05-06 wenzelm 2015-05-06 tuned;
2015-05-06 wenzelm 2015-05-06 less confusing default;
2015-05-06 wenzelm 2015-05-06 proper bib entry;
2015-05-06 wenzelm 2015-05-06 prevent incoherent default in SideKick 1.7;
2015-05-06 blanchet 2015-05-06 corrected path in doc
2015-05-05 wenzelm 2015-05-05 tuned;
2015-05-05 wenzelm 2015-05-05 more documentation;
2015-05-05 wenzelm 2015-05-05 more portable mkdirs via perl, e.g. relevant for Windows UNC paths (network shares);
2015-05-04 wenzelm 2015-05-04 Added tag Isabelle2015-RC3 for changeset e0c3e11e9bea
2015-05-04 wenzelm 2015-05-04 tuned;
2015-05-04 kuncar 2015-05-04 CONTRIBUTORS
2015-05-04 kuncar 2015-05-04 update isar-ref on Lifting
2015-05-04 kuncar 2015-05-04 NEWS
2015-05-04 wenzelm 2015-05-04 tuned;
2015-05-04 wenzelm 2015-05-04 more on GTK;
2015-05-04 wenzelm 2015-05-04 more on Isabelle document preparation and bibtex files;
2015-05-04 wenzelm 2015-05-04 tuned spelling;
2015-05-03 wenzelm 2015-05-03 updated screenshot;
2015-05-03 blanchet 2015-05-03 improved one-line preplaying (don't rely on 'using x by simp' to mean 'by (simp add: x)' and beware of inaccessible '(local.)this')
2015-05-03 blanchet 2015-05-03 made split-rule tactic go beyond constructors with 20 arguments
2015-05-03 wenzelm 2015-05-03 proper fold painter according to jEdit options, not the hardwired default of JEditEmbeddedTextArea;
2015-05-03 wenzelm 2015-05-03 tuned output to resemble input syntax more closely;
2015-05-03 wenzelm 2015-05-03 updated Eisbach, using version fb741500f533 of its Bitbucket repository;
2015-05-03 wenzelm 2015-05-03 proper header;
2015-05-03 wenzelm 2015-05-03 tuned output;
2015-05-03 wenzelm 2015-05-03 tuned output;
2015-05-03 wenzelm 2015-05-03 tuned output;
2015-05-03 wenzelm 2015-05-03 tuned output;
2015-05-03 wenzelm 2015-05-03 tuned output -- avoid empty quites and extra breaks;
2015-05-03 wenzelm 2015-05-03 tuned;
2015-05-03 wenzelm 2015-05-03 suppress formal sort-constraints, in accordance to norm_hhf_eqs;
2015-05-03 wenzelm 2015-05-03 make SML/NJ more happy;
2015-05-03 wenzelm 2015-05-03 tuned message;
2015-05-02 kuncar 2015-05-02 add testing file for code_dt extension of lifting
2015-05-02 kuncar 2015-05-02 handle error messages also in after_qed
2015-05-02 kuncar 2015-05-02 reorder some steps in the construction to support mutual datatypes
2015-05-02 kuncar 2015-05-02 more readable error message if some types do not correspond to sort constraints of the datatype
2015-05-02 kuncar 2015-05-02 better precomputing
2015-05-02 kuncar 2015-05-02 equivalence in code_dt data structure must respect both rty and qty
2015-05-02 kuncar 2015-05-02 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
2015-04-13 kuncar 2015-04-13 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
2014-12-05 kuncar 2014-12-05 Workaround that allows us to execute lifted constants that have as a return type a datatype containing a subtype