Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-30000
-10000
-3000
-1000
-300
-100
-60
+60
+100
+300
+1000
+3000
+10000
+30000
tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or
revset expression
.
The revision graph only works with JavaScript-enabled browsers.
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
less
more
|
(0)
-30000
-10000
-3000
-1000
-300
-100
-60
+60
+100
+300
+1000
+3000
+10000
+30000
tip