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