2010-07-29 |
blanchet |
fix bug with "=" vs. "fequal" introduced by last change (dddb8ba3a1ce)
|
changeset |
files
|
2010-07-29 |
blanchet |
generate correct names for "$true" and "$false";
|
changeset |
files
|
2010-07-29 |
blanchet |
don't assume canonical rule format
|
changeset |
files
|
2010-07-29 |
blanchet |
avoid "clause" and "cnf" terminology where it no longer makes sense
|
changeset |
files
|
2010-07-29 |
blanchet |
"axiom_clauses" -> "axioms" (these are no longer clauses)
|
changeset |
files
|
2010-07-29 |
blanchet |
remove the "extra_clauses" business introduced in 19a5f1c8a844;
|
changeset |
files
|
2010-07-29 |
bulwahn |
adapting output for first solution
|
changeset |
files
|
2010-07-29 |
bulwahn |
removing pointless type information in internal prolog terms
|
changeset |
files
|
2010-07-29 |
bulwahn |
cleaning example file; more natural ordering of variable names
|
changeset |
files
|
2010-07-29 |
bulwahn |
improving translation to prolog; restoring terms from prolog output; adding tracing support
|
changeset |
files
|
2010-07-29 |
bulwahn |
working on parser for prolog reponse
|
changeset |
files
|
2010-07-29 |
bulwahn |
querying for multiple solutions in values command for prolog execution
|
changeset |
files
|
2010-07-29 |
bulwahn |
correcting scanning
|
changeset |
files
|
2010-07-29 |
bulwahn |
adding values command and parsing prolog output
|
changeset |
files
|
2010-07-29 |
bulwahn |
adding example file for prolog code generation; adding prolog code generation example to IsaMakefile
|
changeset |
files
|
2010-07-29 |
bulwahn |
adding a mockup version for prolog code generation
|
changeset |
files
|
2010-07-29 |
bulwahn |
exporting retrieval function for graph of introduction rules in the predicate compiler core
|
changeset |
files
|
2010-07-29 |
haftmann |
merged
|
changeset |
files
|
2010-07-29 |
haftmann |
rebinding ref is illegal
|
changeset |
files
|
2010-07-29 |
haftmann |
tuned example
|
changeset |
files
|
2010-07-29 |
haftmann |
intermediate operation avoids invariance problem in Scala
|
changeset |
files
|
2010-07-29 |
blanchet |
merged
|
changeset |
files
|
2010-07-29 |
blanchet |
kill polymorphic "val"s
|
changeset |
files
|
2010-07-29 |
blanchet |
improved ATP error handling some more
|
changeset |
files
|
2010-07-28 |
blanchet |
shorter URL
|
changeset |
files
|
2010-07-28 |
blanchet |
mention version numbers
|
changeset |
files
|
2010-07-28 |
blanchet |
fiddled with usage text
|
changeset |
files
|
2010-07-28 |
blanchet |
handle Perl and "libwww-perl" failures more gracefully, giving the user some clues about what goes on
|
changeset |
files
|
2010-07-29 |
haftmann |
merged
|
changeset |
files
|
2010-07-29 |
haftmann |
tuned printing of applications and let cascades
|
changeset |
files
|
2010-07-29 |
haftmann |
checking Scala_imp
|
changeset |
files
|
2010-07-29 |
haftmann |
proper unit type in transformed program
|
changeset |
files
|
2010-07-29 |
haftmann |
merged
|
changeset |
files
|
2010-07-28 |
haftmann |
merged
|
changeset |
files
|
2010-07-28 |
haftmann |
tuned; added pretty numerals for code generation
|
changeset |
files
|
2010-07-28 |
haftmann |
may use `int` in Isabelle runtime environment
|
changeset |
files
|
2010-07-28 |
haftmann |
dropped dead code
|
changeset |
files
|
2010-07-28 |
blanchet |
merged
|
changeset |
files
|
2010-07-28 |
blanchet |
make Mirabelle happy
|
changeset |
files
|
2010-07-28 |
blanchet |
renamed environment variable
|
changeset |
files
|
2010-07-28 |
blanchet |
updated component name
|
changeset |
files
|
2010-07-28 |
blanchet |
consequence of directory renaming
|
changeset |
files
|
2010-07-28 |
blanchet |
rename directory
|
changeset |
files
|
2010-07-28 |
blanchet |
minor refactoring
|
changeset |
files
|
2010-07-28 |
blanchet |
minor refactoring
|
changeset |
files
|
2010-07-28 |
blanchet |
updated Sledgehammer docs
|
changeset |
files
|
2010-07-28 |
blanchet |
remove needless "-x" option, now that (1) we can't handle remote SPASS anymore; and (2) we can a priori parse the SPASS syntax in "Sledgehammer_Proof_Reconstruct" anyway
|
changeset |
files
|
2010-07-28 |
blanchet |
remove "remote_spass" because there's no way to find out which clauses come from which facts + rename scripts
|
changeset |
files
|
2010-07-28 |
blanchet |
fix bug in the SPASS Flotter hack, when a conjecture FOF is translated to several CNF clauses
|
changeset |
files
|
2010-07-28 |
blanchet |
revive "e" and "remote_e"'s fact extraction so that it works with E 1.2 as well;
|
changeset |
files
|
2010-07-28 |
blanchet |
more robust proof reconstruction
|
changeset |
files
|
2010-07-28 |
blanchet |
adapt to new (?) TPTP output
|
changeset |
files
|
2010-07-28 |
blanchet |
fix remote_vampire's proof reconstruction
|
changeset |
files
|
2010-07-28 |
blanchet |
fix proof reconstruction for latest Vampire
|
changeset |
files
|
2010-07-28 |
blanchet |
renaming
|
changeset |
files
|
2010-07-28 |
blanchet |
support latest version of Vampire (1.0) locally
|
changeset |
files
|
2010-07-27 |
blanchet |
improve detection of installed SPASS
|
changeset |
files
|
2010-07-28 |
wenzelm |
merged
|
changeset |
files
|
2010-07-27 |
blanchet |
merge
|
changeset |
files
|
2010-07-27 |
blanchet |
compile
|
changeset |
files
|