isabelle: File revisions

src/HOL/Tools/res_atp.ML

2006-08-02	wenzelm	2006-08-02	normalized Proof.context/method type aliases;	file \| diff \| annotate
2006-07-28	paulson	2006-07-28	"all theorems" mode forces definition-expansion off. signature tidying	file \| diff \| annotate
2006-07-27	wenzelm	2006-07-27	moved basic assumption operations from structure ProofContext to Assumption;	file \| diff \| annotate
2006-07-15	mengj	2006-07-15	Pass user lemmas' names to ResHolClause.tptp_write_file and dfg_write_file.	file \| diff \| annotate
2006-07-06	paulson	2006-07-06	some tidying; fixed the output of theorem names	file \| diff \| annotate
2006-06-15	paulson	2006-06-15	the "all_theorems" option and some fixes	file \| diff \| annotate
2006-06-04	mengj	2006-06-04	ATP/res_clasimpset.ML has been merged into res_atp.ML.	file \| diff \| annotate
2006-05-29	paulson	2006-05-29	warnings to debug outputs	file \| diff \| annotate
2006-05-29	paulson	2006-05-29	Giving the "--silent" switch to E, to produce less output	file \| diff \| annotate
2006-05-25	mengj	2006-05-25	Added in settings used by "spass" method.	file \| diff \| annotate
2006-05-25	mengj	2006-05-25	Added support for DFG format, used by SPASS.	file \| diff \| annotate
2006-05-17	paulson	2006-05-17	removing the string array from the result of get_clasimp_atp_lemmas	file \| diff \| annotate
2006-05-16	wenzelm	2006-05-16	replaced low-level Term.str_of by Display.raw_string_of_term (should actually use Display.string_of_term);	file \| diff \| annotate
2006-05-11	wenzelm	2006-05-11	avoid raw equality on type thm;	file \| diff \| annotate
2006-04-28	mengj	2006-04-28	removed the functions for getting HOL helper paths.	file \| diff \| annotate
2006-04-20	mengj	2006-04-20	Changed the logic detection method.	file \| diff \| annotate
2006-04-19	paulson	2006-04-19	exported linkup_logic_mode and changed the default setting	file \| diff \| annotate
2006-04-19	paulson	2006-04-19	tidying; ATP options including CASC mode for Vampire	file \| diff \| annotate
2006-04-18	mengj	2006-04-18	Tidied up some programs.	file \| diff \| annotate
2006-04-07	mengj	2006-04-07	lemmas returned from ResClasimp.get_clasimp_atp_lemmas are thm rather than term.	file \| diff \| annotate
2006-03-09	mengj	2006-03-09	Added more functions to the signature and tidied up some functions.	file \| diff \| annotate
2006-03-07	paulson	2006-03-07	Tidying. New invoke_atp_ml for top-level debugging. Flag to force FOL mode.	file \| diff \| annotate
2006-03-07	mengj	2006-03-07	Merged res_atp_setup.ML into res_atp.ML. HOL translation is integrated with background Isabelle-ATP linkup. Both ATP methods and background linkup retrieve lemmas stored in claset, simpset and atpset.	file \| diff \| annotate
2006-02-09	paulson	2006-02-09	tidying	file \| diff \| annotate
2006-01-31	paulson	2006-01-31	reorganization of code to support DFG otuput	file \| diff \| annotate
2006-01-27	paulson	2006-01-27	tidying up SPASS output	file \| diff \| annotate
2006-01-23	paulson	2006-01-23	ResClasimp.get_clasimp_lemmas now takes all subgoals rather than only the first	file \| diff \| annotate
2006-01-17	paulson	2006-01-17	improved SPASS support	file \| diff \| annotate
2006-01-14	wenzelm	2006-01-14	Output.debug;	file \| diff \| annotate
2006-01-13	paulson	2006-01-13	more practical time limit	file \| diff \| annotate
2005-12-14	paulson	2005-12-14	removed unused function repeat_RS	file \| diff \| annotate
2005-11-28	mengj	2005-11-28	Only output arities and class relations if !ResClause.keep_types is true.	file \| diff \| annotate
2005-10-28	mengj	2005-10-28	Added "writeln_strs" to the signature	file \| diff \| annotate
2005-10-18	paulson	2005-10-18	new interface to make_conjecture_clauses	file \| diff \| annotate
2005-10-14	paulson	2005-10-14	signature changes	file \| diff \| annotate
2005-10-14	paulson	2005-10-14	deletion of Tools/res_types_sorts; removal of absolute numbering of clauses	file \| diff \| annotate
2005-10-10	paulson	2005-10-10	small tidy-up of utility functions	file \| diff \| annotate
2005-10-07	paulson	2005-10-07	minor code tidyig	file \| diff \| annotate
2005-10-07	paulson	2005-10-07	more tidying. Fixed process management bugs and race condition	file \| diff \| annotate
2005-10-06	paulson	2005-10-06	major simplification: removal of the goalstring argument	file \| diff \| annotate
2005-10-05	paulson	2005-10-05	improved process handling. tidied	file \| diff \| annotate
2005-10-04	paulson	2005-10-04	fixed the ascii-armouring of goalstring	file \| diff \| annotate
2005-09-29	paulson	2005-09-29	improvements for problem generation	file \| diff \| annotate
2005-09-28	paulson	2005-09-28	time limit option; fixed bug concerning first line of ATP output	file \| diff \| annotate
2005-09-20	paulson	2005-09-20	tidying, and support for axclass/classrel clauses	file \| diff \| annotate
2005-09-20	paulson	2005-09-20	further tidying; killing of old Watcher loops	file \| diff \| annotate
2005-09-19	paulson	2005-09-19	further simplification of the Isabelle-ATP linkup	file \| diff \| annotate
2005-09-19	paulson	2005-09-19	simplification of the Isabelle-ATP code; hooks for batch generation of problems	file \| diff \| annotate
2005-09-16	paulson	2005-09-16	PARTIAL conversion to Vampire8	file \| diff \| annotate
2005-09-15	paulson	2005-09-15	massive tidy-up and simplification	file \| diff \| annotate
2005-09-15	paulson	2005-09-15	the experimental tagging system, and the usual tidying	file \| diff \| annotate
2005-09-09	paulson	2005-09-09	Isabelle-ATP link: sortable axiom names; no spaces in switches; general tidying	file \| diff \| annotate
2005-09-07	paulson	2005-09-07	Progress on eprover linkup, also massive tidying	file \| diff \| annotate
2005-09-07	paulson	2005-09-07	axioms now included in tptp files, no /bin/cat and various tidying	file \| diff \| annotate
2005-09-02	quigley	2005-09-02	Added ECommunication.ML and modified res_atp.ML, Reconstruction.thy, and recon_transfer_proof.ML to deal with the E theorem prover.	file \| diff \| annotate
2005-09-02	paulson	2005-09-02	further tidying up of Isabelle-ATP link	file \| diff \| annotate
2005-09-02	paulson	2005-09-02	tidying up the Isabelle/ATP interface	file \| diff \| annotate
2005-08-26	quigley	2005-08-26	DFG output now works for untyped rules (ML "ResClause.untyped();")	file \| diff \| annotate
2005-08-17	paulson	2005-08-17	new command to invoke ATPs	file \| diff \| annotate
2005-07-28	paulson	2005-07-28	dead code	file \| diff \| annotate

isabelle

RSS Atom