Mercurial
Mercurial
>
repos
>
isabelle
/ shortlog
summary
| shortlog |
changelog
|
graph
|
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
(0)
-30000
-10000
-3000
-1000
-300
-100
-30
-10
-8
+8
+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
.
Thu, 09 Jun 2011 08:31:41 +0200
bulwahn
local simp rule in List_Cset
changeset
|
files
Thu, 09 Jun 2011 00:16:28 +0200
blanchet
tuning
changeset
|
files
Thu, 09 Jun 2011 00:16:28 +0200
blanchet
compile
changeset
|
files
Thu, 09 Jun 2011 00:16:28 +0200
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)
changeset
|
files
Thu, 09 Jun 2011 00:16:28 +0200
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)
changeset
|
files
Thu, 09 Jun 2011 00:16:28 +0200
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
changeset
|
files
Thu, 09 Jun 2011 00:16:28 +0200
blanchet
removed needless function that duplicated standard functionality, with a little unnecessary twist
changeset
|
files
Thu, 09 Jun 2011 00:16:28 +0200
blanchet
removed more dead code
changeset
|
files
(0)
-30000
-10000
-3000
-1000
-300
-100
-30
-10
-8
+8
+10
+30
+100
+300
+1000
+3000
+10000
+30000
tip