2012-03-23 kuncar 2012-03-23 hide invariant constant
2012-03-24 wenzelm 2012-03-24 explicit SMTP server (appears to be required after recent change of system configuration);
2012-03-24 wenzelm 2012-03-24 more isatest subscribers;
2012-03-23 paulson 2012-03-23 merged
2012-03-23 paulson 2012-03-23 proof tidying
2012-01-16 kuncar 2012-01-16 updated comment
2012-03-23 kuncar 2012-03-23 resolve invariant constant name clash
2012-03-23 kuncar 2012-03-23 update etc/isar-keywords.el
2012-03-23 kuncar 2012-03-23 fix example files
2012-03-23 kuncar 2012-03-23 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
2012-03-23 kuncar 2012-03-23 simplified code of generation of aggregate relations
2012-03-23 kuncar 2012-03-23 store the relational theorem for every relator
2012-03-23 kuncar 2012-03-23 store the quotient theorem for every quotient
2012-03-23 kuncar 2012-03-23 fix Quotient_Examples
2012-03-23 kuncar 2012-03-23 respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
2012-03-23 bulwahn 2012-03-23 adjusting to longer names in PNF_Narrowing_Engine, which was overlooked in 4106258260b3
2012-03-23 wenzelm 2012-03-23 tuned;
2012-03-22 wenzelm 2012-03-22 merged;
2012-03-22 haftmann 2012-03-22 fixed typo
2012-03-22 haftmann 2012-03-22 more instructive NEWS
2012-03-22 paulson 2012-03-22 more structured proofs
2012-03-22 paulson 2012-03-22 New Message
2012-03-22 berghofe 2012-03-22 No longer treat "title" as FDL keyword
2012-03-22 wenzelm 2012-03-22 tuned proofs;
2012-03-22 wenzelm 2012-03-22 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;
2012-03-22 wenzelm 2012-03-22 tuned;
2012-03-22 wenzelm 2012-03-22 synchronize syntax uniformly for target stack and aux. context;
2012-03-22 wenzelm 2012-03-22 tuned;
2012-03-21 wenzelm 2012-03-21 merged
2012-03-21 blanchet 2012-03-21 removed Satallax option, now that this is the default
2012-03-21 blanchet 2012-03-21 doc update
2012-03-21 blanchet 2012-03-21 improve "remote_satallax" by exploiting unsat core
2012-03-21 blanchet 2012-03-21 generate weights and precedences for predicates as well
2012-03-21 paulson 2012-03-21 refinements to constructibility
2012-03-21 paulson 2012-03-21 More structured proofs for infinite cardinalities
2012-03-21 wenzelm 2012-03-21 actually expose target context;
2012-03-21 wenzelm 2012-03-21 more explicit Toplevel.open_target/close_target; replaced 'context_includes' by 'context' 'includes'; tuned command descriptions;
2012-03-21 wenzelm 2012-03-21 tuned signature;
2012-03-21 wenzelm 2012-03-21 optional 'includes' element for long theorem statements; tuned signatures;
2012-03-21 wenzelm 2012-03-21 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;
2012-03-21 wenzelm 2012-03-21 tuned messages;
2012-03-21 wenzelm 2012-03-21 basic support for nested local theory targets;
2012-03-21 wenzelm 2012-03-21 try apple.laf.useScreenMenuBar=false to make menus stay closer to the editor views they belong to -- potentially less confusing for jEdit newcomers;
2012-03-21 wenzelm 2012-03-21 improved isatest arguments for macbroy2;
2012-03-21 wenzelm 2012-03-21 clarified Local_Theory.init: avoid hardwired naming policy, discontinued odd/unused group argument (cf. 5ee13e0428d2); tuned;
2012-03-21 wenzelm 2012-03-21 prefer explicitly qualified exception List.Empty;
2012-03-20 wenzelm 2012-03-20 merged
2012-03-20 wenzelm 2012-03-20 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;
2012-03-20 wenzelm 2012-03-20 basic support for bundled declarations;
2012-03-20 blanchet 2012-03-20 doc update
2012-03-20 blanchet 2012-03-20 made "spass" a "metaprover" that uses either the new SPASS or the old SPASS, to preserve backward compatibility and prepare for the upcoming release
2012-03-20 blanchet 2012-03-20 removed obsolete temporary hack
2012-03-20 blanchet 2012-03-20 tweaks
2012-03-20 paulson 2012-03-20 proof tidying
2012-03-20 wenzelm 2012-03-20 minimalistic support for remote URLs: no master dir here;
2012-03-20 blanchet 2012-03-20 optimized "metis" call
2012-03-20 blanchet 2012-03-20 added term_order option to Mirabelle
2012-03-20 blanchet 2012-03-20 take out experimental polymorphic @ encodings from Metis test -- proof reconstruction is fragile for them
2012-03-20 blanchet 2012-03-20 more conservative Metis defaults, for backward compatiblity (as illustrated by one "metis" call in "Auth/KerberosV")
2012-03-20 blanchet 2012-03-20 remove two options that were found to play hardly any role