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 -14 +14 +100 +300 +1000 +3000 +10000 +30000 tip

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

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

isabelle