tuned signature -- define some elementary operations earlier;

discontinued odd "temporary" workaround from 2006 (6ac7a4fc32a0), which has no measurable relevance;

tuned;

tuned;

tuned;

generic euclidean algorithm (due to Manuel Eberl)

integrated appendix theory into main theory; tuned ML

dropped dead file

fix tactic failure with rel_induct0 minimal example: datatype_new 'a A1 = A1 nat and 'a A2 = A2 'a

added jdk-8u20 (inactive);

proper static closure of ML tactic -- data slot is used twice, for ML compiler and transformed declaration;

support for declaration within token source;

more uniform data slot;

default command position is only valid for default text chunk (amending dcb758188aa6);

tuned -- more total;

tuned;

support for nested Token.src within Token.T; tuned signature;

tuned signature -- moved type src to Token, without aliases;

merged

clarified modules;

added PARALLEL_ALLGOALS convenience;

just one context for Method.evaluate (in contrast to a989bdaf8121, but in accordance to old global situation);

tuned signature;

more compact datatypes;

tuned;

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;