isabelle: File revisions

src/HOL/Metis.thy

2014-02-16	haftmann	2014-02-16	eliminated odd dislocation of keyword declaration and implementation (leftover from 318cd8ac1817)	file \| diff \| annotate
2014-01-30	blanchet	2014-01-30	added 'algebra' and 'meson' to 'try0'	file \| diff \| annotate
2013-10-18	blanchet	2013-10-18	killed more "no_atp"s	file \| diff \| annotate
2013-07-13	wenzelm	2013-07-13	hybrid "auto" tool setup, for TTY (within theory) and PIDE (global print function);	file \| diff \| annotate
2012-08-22	wenzelm	2012-08-22	prefer ML_file over old uses;	file \| diff \| annotate
2012-05-21	blanchet	2012-05-21	add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"	file \| diff \| annotate
2012-03-15	wenzelm	2012-03-15	declare command keywords via theory header, including strict checking outside Pure;	file \| diff \| annotate
2012-02-24	blanchet	2012-02-24	renamed 'try_methods' to 'try0'	file \| diff \| annotate
2012-01-23	blanchet	2012-01-23	renamed two files to make room for a new file	file \| diff \| annotate
2011-11-15	blanchet	2011-11-15	continued implementation of lambda-lifting in Metis	file \| diff \| annotate
2011-09-02	blanchet	2011-09-02	renamed "Metis_Tactics" to "Metis_Tactic", now that there is only one Metis tactic ("metisFT" is legacy)	file \| diff \| annotate
2011-05-31	blanchet	2011-05-31	first step in sharing more code between ATP and Metis translation	file \| diff \| annotate
2011-05-27	blanchet	2011-05-27	renamed "try" "try_methods"	file \| diff \| annotate
2011-05-02	wenzelm	2011-05-02	added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory; proper name bindings;	file \| diff \| annotate
2011-04-14	blanchet	2011-04-14	make 48170228f562 work also with "HO_Reas" examples	file \| diff \| annotate
2010-12-15	blanchet	2010-12-15	added Sledgehammer support for higher-order propositional reasoning	file \| diff \| annotate
2010-12-07	blanchet	2010-12-07	load "try" after "Metis" and move "Async_Manager" back to Sledgehammer	file \| diff \| annotate
2010-10-11	blanchet	2010-10-11	"setup" in theory	file \| diff \| annotate
2010-10-05	blanchet	2010-10-05	hide one more name	file \| diff \| annotate
2010-10-05	blanchet	2010-10-05	hide uninteresting MESON/Metis constants and facts and remove "meson_" prefix to (now hidden) fact names	file \| diff \| annotate
2010-10-04	blanchet	2010-10-04	tuning	file \| diff \| annotate
2010-10-04	blanchet	2010-10-04	move Metis into Plain	file \| diff \| annotate
2007-06-20	wenzelm	2007-06-20	The Metis prover (slightly modified version from Larry);	file \| diff \| annotate

isabelle

RSS Atom