clarifed Method.evaluate: turn text into semantic method (like Basic);

simplified type Proof.method;

more general dummy: may contain "parked arguments", for example;

document 'ctr_transfer'

generate 'ctr_transfer' for (co)datatypes

rename Quickcheck_Types to Lattice_Constructions and remove quickcheck setup

Enum.finite_5 already provides a non-distributive lattice (see 51aa30c9ee4e)

reduced dependency on 'Datatype' theory and ML module

removed Z3 3.2, now superseded by Z3 4.3

avoid old 'smt' method in examples

robustified tactics

tuning

don't note low-level (co)datatype theorems, unless 'bnf_note_all' is set

documented slight incompatibility in NEWS

removed junk

updated docs

set attributes on 'set_cases' theorem

cleaned up derivation of 'sset_induct'

tuning

added collection theorem for consistency and convenience

reordered some (co)datatype property names for more consistency

document 'map_cong_simp'

generate 'map_cong_simp' for BNFs

merged

merged;

Added tag Isabelle2014-RC4 for changeset 113b43b84412

updated to jdk-7u67;

postpone changes in intermediate state between remove_versions/removed_versions, which is important for handle_change to refer to defined items on prover side;

explicit system message for protocol failure -- show on Syslog panel instead of Raw Output; more robust crash recovery: warning could crash again;

added option editor_syslog_limit;

tuned;

updated to cygwin-20140813 -- some version after 1.7.31-3;

document 'inj_map_strong'

generate 'inj_map_strong' for BNFs

note 'inj_map' more often

generate property 'rel_mono_strong' for BNFs

renamed 'rel_mono_strong' to 'rel_mono_strong0'

use 'image_mset' as BNF map function

made SML/NJ happy;

updated to named_theorems;

updated to named_theorems;

updated to named_theorems;

updated to named_theorems;

updated to named_theorems; modernized setup;

updated to named_theorems; modernized module name and setup;

clarified order of rules;

updated to named_theorems; modernized setup; tuned;

updated to named_theorems;

clarified order of arith rules;

clarified order of rules for match_tac/resolve_tac;

updated to named_theorems;

updated to named_theorems;

updated to named_theorems;

updated to named_theorems;

updated to named_theorems;

modernized module name and setup;

updated syntax for localized commands;

updated documentation concerning 'named_theorems';

prefer 'named_theorems' over Named_Thms, with subtle change of semantics due to visual order vs. internal reverse order;

more informative Token.Name with history of morphisms; tuned signature;

merged

more informative Token.Fact: retain name of dynamic fact (without selection);

localized command 'method_setup' and 'attribute_setup'; clarified (non)application of morphism: argument src is already transformed, semantic body remains untransformed;

T1 font encoding with searchable underscore (requires proper cm-super fonts);

prefer high-level change of \isabellestyle;

tuned;

tuned;

tuned signature;

localized method definitions (see also f14c1248d064);

tuned signature -- prefer self-contained user-space tool;

document property 'rel_map'

generate 'rel_map' theorem for BNFs

tuned;

merged

tuned signature -- proper Local_Theory.add_thms_dynamic;

transfer result of Global_Theory.add_thms_dynamic to context stack; more accurate local aliases;

localized attribute definitions;

load local_theory.ML before attrib.ML, with subtle change of semantics due to canonical Local_Theory.map_contexts instead of private Local_Theory.map_top;

clarified terminology: first is top (amending d110b0d1bc12);

tuned whitespace;

tuned comments;

add algebraic type class instances for Enum.finite* types

Quickcheck_Types is no longer needed due to 51aa30c9ee4e

clarified focus and key handling -- more like SideKick; avoid resetting input map with its potentially confusion propagation of key events to unrelated components, e.g. main text area or tree scrollbar;

merged

tuned signature according to Scala version -- prefer explicit argument;

tuned signature;

generic process wrapping in Prover; clarified module arrangement;

more abstract Prover.System_Process, which allows to bypass Isabelle_System.Managed_Process;

allow hyperlinks without offset, just in case the prover emits such reports, despite Position.is_reported;

more frugal standard message properties;

tuned;

clarified Position.Identified: do not require range from prover, default to command position;

maintain Command_Range position as in ML;

more compact representation of special string values;

separate Java FX modules -- no need to include jfxrt.jar by default;

tuned signature;

tuned signature;

separate module Command_Span: mostly syntactic representation; potentially prover-specific Output_Syntax.parse_spans;

tuned signature;

clarified Command_Span in accordance to Scala (see also c2c1e5944536);

tuned output, in accordance to transaction name in ML;

more explicit type Span in Scala, according to ML version;

clarified modules;

clarified signature: entity serial number is not position id;

avoid needless (and wrong w.r.t. sorts) generation of type variables; tuned whitespaces;

improved unfolding of 'let's

tuned whitespace

less aggressive unfolding; removed debugging;

document property 'set_cases'

generate 'set_cases' theorem for (co)datatypes

document property 'set_intros'

generate 'set_intros' theorem for (co)datatypes

use Goal.prove_sorry instead of Goal.prove where possible (= no schematics in goal and tactic is expected to succeed)

reduced warnings;

some localization;

support aliases within the facts space;

support for named collections of theorems in canonical order;

insist in proper 'document_files';

tuned -- avoid confusion with @{assert} for system failures (exception Fail);