tuned proofs;

uniform Generic_Target.standard_declaration, which uses the standard morphism for each context (NB: targets like "interpretation" appear like "theory" but declare local type parameters); uniform treatment of target contexts as invisible; added Local_Theory.standard_form convenience;

tuned;

synchronize syntax uniformly for target stack and aux. context;

tuned;

merged

removed Satallax option, now that this is the default

doc update

improve "remote_satallax" by exploiting unsat core

generate weights and precedences for predicates as well

refinements to constructibility

More structured proofs for infinite cardinalities

actually expose target context;

more explicit Toplevel.open_target/close_target; replaced 'context_includes' by 'context' 'includes'; tuned command descriptions;

tuned signature;

optional 'includes' element for long theorem statements; tuned signatures;

basic support for nested contexts including bundles; include multiple bundles; renamed "affirm" back to "assert" (cf. c4492c6bf450 which was motivated by obsolete Alice/ML); tuned signatures;

tuned messages;

basic support for nested local theory targets;

try apple.laf.useScreenMenuBar=false to make menus stay closer to the editor views they belong to -- potentially less confusing for jEdit newcomers;

improved isatest arguments for macbroy2;

clarified Local_Theory.init: avoid hardwired naming policy, discontinued odd/unused group argument (cf. 5ee13e0428d2); tuned;

prefer explicitly qualified exception List.Empty;

merged

refined init_model: allow change of buffer name as caused by "Save as", for example; avoid init_model while buffer.isLoading -- potentially prevent NPE of getText; avoid emitting nested buffer.propertiesChanged events;

basic support for bundled declarations;

doc update

made "spass" a "metaprover" that uses either the new SPASS or the old SPASS, to preserve backward compatibility and prepare for the upcoming release

removed obsolete temporary hack

tweaks

proof tidying

minimalistic support for remote URLs: no master dir here;

optimized "metis" call

added term_order option to Mirabelle

take out experimental polymorphic @ encodings from Metis test -- proof reconstruction is fragile for them

more conservative Metis defaults, for backward compatiblity (as illustrated by one "metis" call in "Auth/KerberosV")

remove two options that were found to play hardly any role

enable "metis_advisory_simp" by default

more stats;

merged

more structured proofs

don't generate new SPASS constructs for old SPASS

tune Metis example

added "metis_advisory_simp" option to orient as many equations as possible in Metis the right way (cf. "More SPASS with Isabelle")

continued implementation of term ordering attributes

added "dont_preplay" alias

document "dont_preplay"

tuning

implement term order attribute (for experiments)

tuning -- don't refer to old, internal version number (needlessly confusing now)

more weight attribute tuning

use TFF0 with remote Vampire, now that a newer version of Vampire has been installed there (1.8 rev. 1362) that appears to have sound support for TFF0

internal renamings

renamed E weight attribute

tuned proofs;

explicit propagation of assignment event, even if changed command set is empty; discontinued slightly odd Document_View.update_snapshot/flush_snapshot;

modernized axiomatizations;

modernized axiomatizations; tuned proofs;

updated Misc_Legacy.freeze_thaw;

discontinued remains of duplicate exception UnequalLengths (cf. 441260986b63);

moved some legacy stuff;

clarified Binding.name_of vs Name_Space.base_name vs Variable.check_name (see also 9bd8d4addd6e, 3305f573294e);

merged

merged

More structured proofs for cardinalities

merged

more structured case and induction proofs

better defaults for Metis, that seem to make it less likely to loop seemingly forever -- 0 coefficients might very well make it incomplete

allow keyword tags to be redefined, but not the command category;

further amendment of "updated" edge (cf. 6ed49c52d463) -- required for repainting of unassigned command, e.g. for inactive buffe;

clarified command span classification: strict Command.is_command, permissive Command.name;

more robust bash interpolation;

more ambitious scalac options for makedist;

less noisy Isabelle/Scala build process;

comment;

tuned;

tuned;

maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming); more explicit Context.generic for Name_Space.declare/define and derivatives (NB: naming changed after Proof_Context.init_global); prefer Context.pretty in low-level operations of structure Sorts/Type (defer full Syntax.init_pretty until error output); simplified signatures;

tuned;

tuned structure;

comments for uniformity

proper naming of simprocs according to actual target context; afford pervasive declaration which makes results available with qualified name from outside;

amended locale_declaration: avoid duplication of Local_Theory.target with global_morphism (cf. 57def0b39696) -- Haftmann-Wenzel Sandwich has 3 layers, not 4;

more precise syntax;

more antiquotations;

misc tuning to accomodate scala-2.10.0-M2;

include scala.xml as of scala-2.9.1.final/misc/scala-tool-support/jedit/modes/scala.xml -- seems to be missing in more recent distributions;

merged

merged

tidying and structured proofs

refined Local_Theory.define vs. Local_Theory.define_internal, which allows to pass alternative name to the foundational axiom -- expecially important for 'instantiation' or 'overloading', which loose name information due to Long_Name.base_name cooking etc.; actually make "raw_def" internal (cf. 80123a220219);

tuned proofs;

simultaneous read_fields -- e.g. relevant for sort assignment;

added Syntax.read_typs; tuned parallelism for syntax operations;

renamed HOL-Matrix to HOL-Matrix_LP to avoid name clash with AFP;

tuned message;

tuned proofs;

tuned proofs;

tuned exception;

merged;

spelt out missing colemmas

generalized INF_INT_eq, SUP_UN_eq

tuned specifications

sort via string_ord (as secondary key), not fast_string_ord via Symtab.fold; tuned;

tuned grouping -- merely indicate order of magnitude;

slightly more parallel find_theorems;

'definition' no longer exports the foundational "raw_def";

some attempts to fit source on screen;

eliminated odd 'finalconsts' / Theory.add_finals;

modernized axiomatization; eliminated odd 'finalconsts';

modernized axiomatization; eliminated odd 'finalconsts';

afford strict Args.type_name (cf. 29e88714ffe4);