isabelle: Graph

merged
2012-03-26, by kuncar
tuned proof - no smt call
2012-03-26, by kuncar
more robust command invocation via ISABELLE_JDK_HOME or SCALA_HOME (NB: bash exec requires genuine executable, not function);
2012-03-26, by wenzelm
updated theory header syntax and related details;
2012-03-26, by wenzelm
ISABELLE_JDK_HOME settings variable points to JDK with javac and jar (not just JRE);
2012-03-24, by wenzelm
merged
2012-03-26, by wenzelm
reintroduced broken proofs and regenerated certificates
2012-03-26, by blanchet
merged, resolving trivial conflict;
2012-03-26, by wenzelm
fixed Nitpick after numeral representation change (2a1953f0d20d)
2012-03-26, by blanchet
merged fork with new numeral representation (see NEWS)
2012-03-25, by huffman
merged
2012-03-24, by kuncar
use Thm.transfer for thms stored in generic context data storage
2012-03-23, by kuncar
hide invariant constant
2012-03-23, by kuncar
explicit SMTP server (appears to be required after recent change of system configuration);
2012-03-24, by wenzelm
more isatest subscribers;
2012-03-24, by wenzelm
merged
2012-03-23, by paulson
proof tidying
2012-03-23, by paulson
updated comment
2012-01-16, by kuncar
resolve invariant constant name clash
2012-03-23, by kuncar
update etc/isar-keywords.el
2012-03-23, by kuncar
fix example files
2012-03-23, by kuncar
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, by kuncar
simplified code of generation of aggregate relations
2012-03-23, by kuncar
store the relational theorem for every relator
2012-03-23, by kuncar
store the quotient theorem for every quotient
2012-03-23, by kuncar
fix Quotient_Examples
2012-03-23, by kuncar
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
2012-03-23, by kuncar
adjusting to longer names in PNF_Narrowing_Engine, which was overlooked in 4106258260b3
2012-03-23, by bulwahn
tuned;
2012-03-23, by wenzelm
merged;
2012-03-22, by wenzelm
fixed typo
2012-03-22, by haftmann
more instructive NEWS
2012-03-22, by haftmann
more structured proofs
2012-03-22, by paulson
New Message
2012-03-22, by paulson
No longer treat "title" as FDL keyword
2012-03-22, by berghofe
tuned proofs;
2012-03-22, by wenzelm
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);
2012-03-22, by wenzelm
tuned;
2012-03-22, by wenzelm
synchronize syntax uniformly for target stack and aux. context;
2012-03-22, by wenzelm
tuned;
2012-03-22, by wenzelm
merged
2012-03-21, by wenzelm
removed Satallax option, now that this is the default
2012-03-21, by blanchet
doc update
2012-03-21, by blanchet
improve "remote_satallax" by exploiting unsat core
2012-03-21, by blanchet
generate weights and precedences for predicates as well
2012-03-21, by blanchet
refinements to constructibility
2012-03-21, by paulson
More structured proofs for infinite cardinalities
2012-03-21, by paulson
actually expose target context;
2012-03-21, by wenzelm
more explicit Toplevel.open_target/close_target;
2012-03-21, by wenzelm
tuned signature;
2012-03-21, by wenzelm
optional 'includes' element for long theorem statements;
2012-03-21, by wenzelm
basic support for nested contexts including bundles;
2012-03-21, by wenzelm
tuned messages;
2012-03-21, by wenzelm
basic support for nested local theory targets;
2012-03-21, by wenzelm
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, by wenzelm
improved isatest arguments for macbroy2;
2012-03-21, by wenzelm
clarified Local_Theory.init: avoid hardwired naming policy, discontinued odd/unused group argument (cf. 5ee13e0428d2);
2012-03-21, by wenzelm
prefer explicitly qualified exception List.Empty;
2012-03-21, by wenzelm
merged
2012-03-20, by wenzelm
refined init_model: allow change of buffer name as caused by "Save as", for example;
2012-03-20, by wenzelm
basic support for bundled declarations;
2012-03-20, by wenzelm
doc update
2012-03-20, by blanchet
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, by blanchet
removed obsolete temporary hack
2012-03-20, by blanchet
tweaks
2012-03-20, by blanchet
proof tidying
2012-03-20, by paulson
minimalistic support for remote URLs: no master dir here;
2012-03-20, by wenzelm
optimized "metis" call
2012-03-20, by blanchet
added term_order option to Mirabelle
2012-03-20, by blanchet
take out experimental polymorphic @ encodings from Metis test -- proof reconstruction is fragile for them
2012-03-20, by blanchet
more conservative Metis defaults, for backward compatiblity (as illustrated by one "metis" call in "Auth/KerberosV")
2012-03-20, by blanchet
remove two options that were found to play hardly any role
2012-03-20, by blanchet
enable "metis_advisory_simp" by default
2012-03-20, by blanchet
more stats;
2012-03-20, by wenzelm
merged
2012-03-20, by paulson
more structured proofs
2012-03-20, by paulson
don't generate new SPASS constructs for old SPASS
2012-03-20, by blanchet
tune Metis example
2012-03-20, by blanchet
added "metis_advisory_simp" option to orient as many equations as possible in Metis the right way (cf. "More SPASS with Isabelle")
2012-03-20, by blanchet
continued implementation of term ordering attributes
2012-03-20, by blanchet
added "dont_preplay" alias
2012-03-20, by blanchet
document "dont_preplay"
2012-03-20, by blanchet
tuning
2012-03-20, by blanchet
implement term order attribute (for experiments)
2012-03-20, by blanchet
tuning -- don't refer to old, internal version number (needlessly confusing now)
2012-03-20, by blanchet
more weight attribute tuning
2012-03-20, by blanchet
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
2012-03-20, by blanchet
internal renamings
2012-03-20, by blanchet
renamed E weight attribute
2012-03-20, by blanchet
tuned proofs;
2012-03-19, by wenzelm
explicit propagation of assignment event, even if changed command set is empty;
2012-03-19, by wenzelm
modernized axiomatizations;
2012-03-19, by wenzelm
modernized axiomatizations;
2012-03-19, by wenzelm
updated Misc_Legacy.freeze_thaw;
2012-03-19, by wenzelm
discontinued remains of duplicate exception UnequalLengths (cf. 441260986b63);
2012-03-19, by wenzelm
moved some legacy stuff;
2012-03-19, by wenzelm
clarified Binding.name_of vs Name_Space.base_name vs Variable.check_name (see also 9bd8d4addd6e, 3305f573294e);
2012-03-19, by wenzelm
merged
2012-03-19, by wenzelm
merged
2012-03-19, by paulson
More structured proofs for cardinalities
2012-03-19, by paulson
merged
2012-03-19, by paulson
more structured case and induction proofs
2012-03-16, by paulson
better defaults for Metis, that seem to make it less likely to loop seemingly forever -- 0 coefficients might very well make it incomplete
2012-03-19, by blanchet
allow keyword tags to be redefined, but not the command category;
2012-03-19, by wenzelm
further amendment of "updated" edge (cf. 6ed49c52d463) -- required for repainting of unassigned command, e.g. for inactive buffe;
2012-03-19, by wenzelm
clarified command span classification: strict Command.is_command, permissive Command.name;
2012-03-19, by wenzelm
more robust bash interpolation;
2012-03-18, by wenzelm
more ambitious scalac options for makedist;
2012-03-18, by wenzelm
less noisy Isabelle/Scala build process;
2012-03-18, by wenzelm
comment;
2012-03-18, by wenzelm
tuned;
2012-03-18, by wenzelm
tuned;
2012-03-18, by wenzelm
maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
2012-03-18, by wenzelm
tuned;
2012-03-18, by wenzelm
tuned structure;
2012-03-18, by wenzelm
comments for uniformity
2012-03-18, by haftmann
proper naming of simprocs according to actual target context;
2012-03-17, by wenzelm
amended locale_declaration: avoid duplication of Local_Theory.target with global_morphism (cf. 57def0b39696) -- Haftmann-Wenzel Sandwich has 3 layers, not 4;
2012-03-17, by wenzelm
more precise syntax;
2012-03-17, by wenzelm
more antiquotations;
2012-03-17, by wenzelm