Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-30000
-10000
-3000
-1000
-300
-100
-15
+15
+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.
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
2012-05-16, by kuncar
infrastructure that makes possible to prove that a relation is reflexive
2012-05-16, by kuncar
temporarily disable "ext" rule helpers until Metis supports them (and until they are properly evaluated)
2012-05-16, by blanchet
lower skolem penalty to ensure that some useful facts with existentials, e.g. congruence of "setsum", eventually get picked up
2012-05-16, by blanchet
treat sets specially in relevance filter, as they used to, to avoid cluttering the problem with facts about Set.member and Collect
2012-05-16, by blanchet
get ready for automatic generation of extensionality helpers
2012-05-16, by blanchet
minor slice tweaking (swapped two slices to move polymorphic encoding up a bit)
2012-05-16, by blanchet
more helpful error message
2012-05-16, by blanchet
transfer rules for many more list constants
2012-05-15, by huffman
made SML/NJ happy
2012-05-15, by blanchet
repair the Waldmeister endgame only for Waldmeister proofs
2012-05-15, by blanchet
fixed Waldmeister commutativity hack
2012-05-15, by blanchet
imported patch atp_tuning
2012-05-15, by blanchet
add transfer rules for nat_rec and funpow
2012-05-15, by huffman
add transfer rule for constant List.lists
2012-05-14, by huffman
less
more
|
(0)
-30000
-10000
-3000
-1000
-300
-100
-15
+15
+100
+300
+1000
+3000
+10000
+30000
tip