Mercurial
Mercurial
>
repos
>
isabelle
/ shortlog
summary
| shortlog |
changelog
|
graph
|
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
(0)
-30000
-10000
-3000
-1000
-300
-100
-30
-10
-7
+7
+10
+30
+100
+300
+1000
+3000
+10000
+30000
tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or
revset expression
.
Wed, 16 May 2012 19:17:20 +0200
kuncar
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
changeset
|
files
Wed, 16 May 2012 19:15:45 +0200
kuncar
infrastructure that makes possible to prove that a relation is reflexive
changeset
|
files
Wed, 16 May 2012 18:16:51 +0200
blanchet
temporarily disable "ext" rule helpers until Metis supports them (and until they are properly evaluated)
changeset
|
files
Wed, 16 May 2012 18:16:51 +0200
blanchet
lower skolem penalty to ensure that some useful facts with existentials, e.g. congruence of "setsum", eventually get picked up
changeset
|
files
Wed, 16 May 2012 18:16:51 +0200
blanchet
treat sets specially in relevance filter, as they used to, to avoid cluttering the problem with facts about Set.member and Collect
changeset
|
files
Wed, 16 May 2012 18:16:51 +0200
blanchet
get ready for automatic generation of extensionality helpers
changeset
|
files
Wed, 16 May 2012 18:16:51 +0200
blanchet
minor slice tweaking (swapped two slices to move polymorphic encoding up a bit)
changeset
|
files
(0)
-30000
-10000
-3000
-1000
-300
-100
-30
-10
-7
+7
+10
+30
+100
+300
+1000
+3000
+10000
+30000
tip