merged

proof tidying

updated comment

resolve invariant constant name clash

update etc/isar-keywords.el

fix example files

generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem

simplified code of generation of aggregate relations

store the relational theorem for every relator

store the quotient theorem for every quotient

fix Quotient_Examples

respectfulness theorem has to be proved if a new constant is lifted by quotient_definition

adjusting to longer names in PNF_Narrowing_Engine, which was overlooked in 4106258260b3

tuned;

merged;

fixed typo

more instructive NEWS

more structured proofs

New Message

No longer treat "title" as FDL keyword

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