replace lemma with more general simp rule

generalized tactics

renamed generated property

commented out debugging output in "primcorec"

merged

tuned proofs;

more quasi-generic PIDE modules (NB: Swing/JFX needs to be kept separate from non-GUI material);

NEWS;

clarified font;

simplified default L&F -- Nimbus should be always available and GTK+ is not fully working yet;

proper platform-specific test;

disable standard behaviour of Mac OS X text field (i.e. select-all after focus gain) in order to make completion work more smoothly;

focus text field, to capture key events even on Mac OS X look-and-feel;

tuned proofs;

more tolerant treatment of end-of-buffer -- avoid debatable situations of jEdit buffer boundaries;

skip ignored commands, similar to former proper_command_at (see d68ea01d5084) -- relevant to Output, Query_Operation etc.; tuned signature;

clarified command spans (again, see also 03a2dc9e0624): restrict to proper range to allow Isabelle.command_edit adding material monotonically without destroying the command (e.g. relevant for sendback from sledgehammer); simplified command padding: always newline, despite lack of indentation;

tuned proofs;

obsolete;

tuned;

avoid clash of auto print functions with query operations, notably sledgehammer (cf. 3461985dcbc3);

tuned isatest options;

updated docs

added [dest] to "disc_exclude"

started adding support for "nat_case" as case study for all "case" constructs

temporary fix to tactic

made SML/NJ happy

tuning

support "of" syntax to disambiguate selector equations

don't note more induction principles than there are functions + tuning

more (co)data docs

improved rail diagram

use "primcorec" in example

use "primcorec" in doc

updated keywords

updated certificates

when "max_thm_instances" is hit, choose more carefully which instances should be kept

add "primcorec" command (cf. ae7f50e70c09)

merged

added lemmas

honor MaSh's zero-overhead policy -- no learning if the tool is disabled

adapted to reflect renaming of session

merged

make measure_of total

encode goal digest in spying log (to detect duplicates)

made SML/NJ happy

tuned proofs

use forthcoming "primcorec" command

set code and nitpick_simp attributes on primcorec theorems

tuning

tuned docs

register codatatypes with Nitpick

register codatatypes with Nitpick

don't generalize w.r.t. wrong context -- better overgeneralize (since the instantiation phase will compensate for it)

added [code] to selectors

tuned spying

document "spy"

added "spy" option to Nitpick

document "spy" option

added "spy" option to Sledgehammer

proper text for document preparation;

set [code] on case equations

note coinduct theorems in "primcorec"

tuning

generate "simps" from "primcorec"

undid copy-paste

avoid giving same name to simplifying constructor as to real one (to avoid risks of confusion when reading the code)

don't generate empty theorem collections

tuned code

provide a way to override MaSh's port from configuration file

new version of MaSh program, with proper shutdown

tuned proofs;

focus on default component according to jEdit window management;

tuned;

tuned signature;

completion popup for history text field; imitate view font, for default rendering of symbols; tuned signature;

clarified location of GUI modules (which depend on Swing of JFX);

repaired latex (cf. 7bb0cf27c243);

tuned proofs;

caret range of active text area counts as visible (e.g. relevant for Output after scrolling outside of text view);

tuned;

proper layered pane at root of parent component, not global view (e.g. relevant for tooltips for detached info windows);

immediate access to some elementary examples;

more front-matter;

clarified logo;

proper text replacement (cf. 747835eb2782);

added canonical screenshot;

removed obsolete README; open Documentation dockable by default;

tuned;

added/updated material from src/Tools/jEdit/README.html;

basic setup for Isabelle/jEdit documentation;

updated keywords;

updated CONTRIBUTORS

updated NEWS

document option

merged "isar_try0" and "isar_minimize" options

hardcoded obscure option

hard-coded an obscure option

use configuration mechanism for low-level tracing

moved focus to Isabell/jEdit and away from Proof General

took out Waldmeister from list of default provers -- it's usually just visual noise, and its integration in Sledgehammer leaves much to be desired

tuning (use a blacklist instead of a whitelist)

reduce the number of emitted MaSh commands (among others to facilitate debugging)

MaSh tweaks to facilitate debugging

tuned proofs

make SML/NJ happy

renamed "primcorec" to "primcorecursive", to open the door to a 'theory -> theory' command called "primcorec" (cf. "fun" vs. "function")

more primcorec docs

added primcorec examples with lambdas

more primcorec docs

adapted primcorec documentation to reflect the three views

updated docs

took out spurious attributes (no need for several code equations / simps for thesame constants)

have "datatype_new_compat" register induction and recursion theorems in nested case

prefer Code.abort over code_abort

setting the stage for safe constructor simp rules

added TODO

made tactic more reliable

killed exceptional code that is anyway no longer needed, now that the 'simp' attribute has been taken away -- this solves issues in 'primcorec'

cleaner handling of collapse theorems