avoid "clause" and "cnf" terminology where it no longer makes sense

"axiom_clauses" -> "axioms" (these are no longer clauses)

remove the "extra_clauses" business introduced in 19a5f1c8a844; it isn't working reliably because of: * relevance_override * it is ignored anyway by TPTP generator A better solution would/will be to ensure monotonicity: extra axioms not used in an ATP proof shouldn't make the rest of the problem provable

adapting output for first solution

removing pointless type information in internal prolog terms

cleaning example file; more natural ordering of variable names

improving translation to prolog; restoring terms from prolog output; adding tracing support

working on parser for prolog reponse

querying for multiple solutions in values command for prolog execution

correcting scanning

adding values command and parsing prolog output

adding example file for prolog code generation; adding prolog code generation example to IsaMakefile

adding a mockup version for prolog code generation

exporting retrieval function for graph of introduction rules in the predicate compiler core

merged

rebinding ref is illegal

tuned example

intermediate operation avoids invariance problem in Scala

merged

kill polymorphic "val"s

improved ATP error handling some more

shorter URL

mention version numbers

fiddled with usage text

handle Perl and "libwww-perl" failures more gracefully, giving the user some clues about what goes on

merged

tuned printing of applications and let cascades

checking Scala_imp

proper unit type in transformed program

merged