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
.
Wed, 12 May 2010 23:53:59 +0200
boehmes
split monolithic Z3 proof reconstruction structure into separate structures, use one set of schematic theorems for all uncertain proof rules (to extend proof reconstruction by missing cases), added several schematic theorems, improved abstraction of goals (abstract all uninterpreted sub-terms, only leave builtin symbols)
changeset
|
files
Wed, 12 May 2010 23:53:58 +0200
boehmes
added tracing of reconstruction data
changeset
|
files
Wed, 12 May 2010 23:53:57 +0200
boehmes
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
changeset
|
files
Wed, 12 May 2010 23:53:56 +0200
boehmes
deleted SMT translation files (to be replaced by a simplified version)
changeset
|
files
Wed, 12 May 2010 23:53:55 +0200
boehmes
move the addition of extra facts into a separate module
changeset
|
files
Wed, 12 May 2010 23:53:54 +0200
boehmes
normalize numerals: also rewrite Numeral0 into 0
changeset
|
files
Wed, 12 May 2010 23:53:53 +0200
boehmes
added missing rewrite rules for natural min and max
changeset
|
files
Wed, 12 May 2010 23:53:52 +0200
boehmes
rewrite bool case expressions as if expression
changeset
|
files
(0)
-30000
-10000
-3000
-1000
-300
-100
-30
-10
-8
+8
+10
+30
+100
+300
+1000
+3000
+10000
+30000
tip