tuned

break more conjunctions

move useful functions to library

merge

simplified code

add non-corecursive constructor view theorems to simps

merged

tuned proofs;

explicit Status.REMOVED, which is required e.g. for sledgehammer to retrieve command of sendback exec_id (in contrast to find_theorems, see c2da0d3b974d);

more powerful fold

properly fold over branches

tuned

removed dead code

keep a database of free constructor type information

generalized case-handling code a bit

support cases for new-style (co)datatypes

use case rather than sequence of ifs in expansion

textual improvements following Christian Sternagel's feedback

generalize lemma

removed unused lemma

factor out new lemma

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