Revision abe86b3bd7551ad3c85a23a6421934f18491d45f authored by cdunchev@gmail.com on 27 August 2012, 22:13:09 UTC, committed by cdunchev@gmail.com on 27 August 2012, 22:13:09 UTC
i.e. the new algorithms to work on the older examples, some type-casting has been done. An interesting question is why the BetaNormalization fails now, for example: // require( betaNormalize( App(Abs(v, f), ub) ) == auxf.formula ) fails as well as all requirements in slk.scala fail. The only change is that auxf.formula is not a SchemaFormula anymore, but a HOLFormula. git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1171 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
1 parent 6f1e9be
File | Mode | Size |
---|---|---|
algorithms | ||
applet | ||
cli | ||
dependencies | ||
gui | ||
integration_tests | ||
parsing | ||
provers | ||
syntax | ||
testing | ||
transformations | ||
ui | ||
utils | ||
cli.sh | -rw-r--r-- | 896 bytes |
gui-cli.sh | -rw-r--r-- | 1.4 KB |
gui.sh | -rw-r--r-- | 860 bytes |
pom.xml | -rw-r--r-- | 5.5 KB |
test_gapt.sh | -rwxr-xr-x | 360 bytes |
Computing file changes ...