isabelle: Graph

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

modernized structure ProofContext;
2011-06-08, by wenzelm
even more robust \isaspacing;
2011-06-09, by wenzelm
simplified Name.variant -- discontinued builtin fold_map;
2011-06-09, by wenzelm
some attempts at robust \isaspacing so that \isa{...} can be used in section headings etc. (need to avoid `\? for some reason);
2011-06-09, by wenzelm
discontinued Name.variant to emphasize that this is old-style / indirect;
2011-06-09, by wenzelm
prefer new-style Name.invents;
2011-06-09, by wenzelm
more tight name invention -- avoiding old functions;
2011-06-09, by wenzelm
\frenchspacing for formal isabelle style avoids extra space in situations like ``@{text "?"}'' followed by plain text;
2011-06-09, by wenzelm
tuned;
2011-06-09, by wenzelm
NEWS
2011-06-09, by bulwahn
correcting import theory of examples
2011-06-09, by bulwahn
fixing code generation test
2011-06-09, by bulwahn
removing char setup
2011-06-09, by bulwahn
removing unneccessary manual instantiations and dead definitions; hiding more constants and facts
2011-06-09, by bulwahn
adding a nicer error message for quickcheck_narrowing; hiding fact empty_def
2011-06-09, by bulwahn
adding narrowing engine for existentials
2011-06-09, by bulwahn
adapting Quickcheck_Narrowing: adding setup for characters; correcting import statement
2011-06-09, by bulwahn
adding theory Quickcheck_Narrowing to HOL-Main image
2011-06-09, by bulwahn
adapting IsaMakefile
2011-06-09, by bulwahn
moving Quickcheck_Narrowing from Library to base directory
2011-06-09, by bulwahn
compilation of Haskell in its own target for Quickcheck; passing options by arguments in Narrowing_Generators
2011-06-09, by bulwahn
local simp rule in List_Cset
2011-06-09, by bulwahn
tuning
2011-06-09, by blanchet
compile
2011-06-09, by blanchet
cleaner fact freshening, which also works in corner cases, e.g. if two backquoted facts have the same name (but have different variable indices)
2011-06-09, by blanchet
added a really fully typed translation as a fallback for Metis, in rare cases where Metis correctly proves a theorem but has type-unsound steps in it (which is likelier to happen with some of the lighter translations)
2011-06-09, by blanchet
improve sort inference in Metis proofs -- in some rare cases Metis steals Isabelle's variable names and the sorts must then be inferred as well
2011-06-09, by blanchet
removed needless function that duplicated standard functionality, with a little unnecessary twist
2011-06-09, by blanchet
removed more dead code
2011-06-09, by blanchet
be a bit more liberal with respect to the universal sort -- it sometimes help
2011-06-09, by blanchet
renamed "untyped_aconv" to distinguish it clearly from the standard "aconv_untyped"
2011-06-09, by blanchet
merged
2011-06-08, by wenzelm
avoid duplicate facts, which confuse the minimizer output
2011-06-08, by blanchet
pass Metis facts and negated conjecture as facts, with (almost) correctly set localities, so that the correct encoding is used for nonmonotonic occurrences of infinite types
2011-06-08, by blanchet
restore comment about subtle issue
2011-06-08, by blanchet
made "query" type systes a bit more sound -- local facts, e.g. the negated conjecture, may make invalid the infinity check, e.g. if we are proving that there exists two values of an infinite type, we can use the negated conjecture that there is only one value to derive unsound proofs unless the type is properly encoded
2011-06-08, by blanchet
don't launch the automatic minimizer for zero facts
2011-06-08, by blanchet
don't generate unsound proof error for missing proofs
2011-06-08, by blanchet
renamed option to avoid talking about seconds, since this is now the default Isabelle unit
2011-06-08, by blanchet
fixed format selection logic for Waldmeister
2011-06-08, by blanchet
better default type system for Waldmeister, with fewer predicates (for types or type classes)
2011-06-08, by blanchet
simplified directory structure;
2011-06-08, by wenzelm
simplified directory structure;
2011-06-08, by wenzelm
further jedit build option;
2011-06-08, by wenzelm
build jedit as part of regular startup script (in that case depending on jedit_build component);
2011-06-08, by wenzelm
updated headers;
2011-06-08, by wenzelm
moved sources -- eliminated Netbeans artifact of jedit package directory;
2011-06-08, by wenzelm
removed obsolete Netbeans project setup;
2011-06-08, by wenzelm
support fresh build of jars;
2011-06-08, by wenzelm
more jvmpath wrapping for Cygwin;
2011-06-08, by wenzelm
more robust exception pattern General.Subscript;
2011-06-08, by wenzelm
pervasive Output operations;
2011-06-08, by wenzelm
modernized Proof_Context;
2011-06-08, by wenzelm
standardized header;
2011-06-08, by wenzelm
merged
2011-06-08, by boehmes
updated SMT certificates
2011-06-08, by boehmes
only collect substituions neither seen before nor derived in the same refinement step
2011-06-08, by boehmes
updated imports (cf. 93b1183e43e5);
2011-06-08, by wenzelm
merged
2011-06-08, by wenzelm
new Metis version
2011-06-08, by blanchet

less more | (0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip

isabelle