removed obsolete RC tags;

merged

Added tag Isabelle2014 for changeset 8f4a332500e4

merged

more explicit Method.modifier with reported position;

tuned signature -- prefer quasi-abstract Symbol_Pos.source;

added ML antiquotation @{source} for Symbol_Pos.source;

tuned signature;

removed not so interesting 'set_empty'

avoid 'PolyML.makestring'

introduce real_of typeclass for real :: 'a => real

added lemmas

better linarith support for floor, ceiling, natfloor, and natceiling

add testing framework for generated code

correct code equation for term_of on integer

merged

add code equation for term_of on integer

added lemmas contributed by Rene Thiemann

attach modifier only later, to avoid interference as e.g. in "simp add: foo [simplified] bar";

tuned whitespace;

clarified ML toplevel pp: avoid ML output to be attached to inlined binding positions;

merged

made SML/NJ happy;

clarified Method.section: explicit declaration with static closure;

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;