isabelle: File revisions

src/Sequents/prover.ML

2010-08-17	haftmann	2010-08-17	more antiquotations	file \| diff \| annotate
2009-10-21	haftmann	2009-10-21	curried inter as canonical list operation (beware of argument order)	file \| diff \| annotate
2009-10-21	haftmann	2009-10-21	dropped redundant gen_ prefix	file \| diff \| annotate
2009-10-17	wenzelm	2009-10-17	eliminated hard tabulators, guessing at each author's individual tab-width; tuned headers;	file \| diff \| annotate
2009-09-29	wenzelm	2009-09-29	explicit indication of Unsynchronized.ref;	file \| diff \| annotate
2009-07-21	wenzelm	2009-07-21	proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;	file \| diff \| annotate
2008-12-31	wenzelm	2008-12-31	moved term order operations to structure TermOrd (cf. Pure/term_ord.ML); tuned signature of structure Term;	file \| diff \| annotate
2008-05-17	wenzelm	2008-05-17	structure Display: less pervasive operations;	file \| diff \| annotate
2007-02-26	wenzelm	2007-02-26	moved eq_thm etc. to structure Thm in Pure/more_thm.ML;	file \| diff \| annotate
2006-11-21	wenzelm	2006-11-21	removed legacy ML setup;	file \| diff \| annotate
2006-10-10	haftmann	2006-10-10	gen_rem(s) abandoned in favour of remove / subtract	file \| diff \| annotate
2006-01-19	wenzelm	2006-01-19	setup: theory -> theory;	file \| diff \| annotate
2005-06-17	wenzelm	2005-06-17	accomodate change of TheoryDataFun; accomodate identification of type Sign.sg and theory;	file \| diff \| annotate
2002-05-07	wenzelm	2002-05-07	use eq_thm_prop instead of slightly inadequate eq_thm;	file \| diff \| annotate
2001-11-28	wenzelm	2001-11-28	theory data: removed obsolete finish method;	file \| diff \| annotate
2001-11-09	wenzelm	2001-11-09	theory data: finish method;	file \| diff \| annotate
1999-08-02	wenzelm	1999-08-02	cat_lines;	file \| diff \| annotate
1999-07-28	paulson	1999-07-28	renamed ...thm_pack... to ...pack...	file \| diff \| annotate
1999-07-27	paulson	1999-07-27	moved the modal prover to modal.ML; installed the prover using TheoryDataFun	file \| diff \| annotate
1998-12-28	paulson	1998-12-28	added new arg for print_tac	file \| diff \| annotate
1997-12-19	wenzelm	1997-12-19	adapted to new sort function;	file \| diff \| annotate
1997-10-20	wenzelm	1997-10-20	adapted to qualified names;	file \| diff \| annotate
1997-07-22	paulson	1997-07-22	Removal of the tactical STATE	file \| diff \| annotate
1996-10-09	paulson	1996-10-09	New unified treatment of sequent calculi by Sara Kalvala combines the old LK and Modal with the new ILL (Int. Linear Logic)	file \| diff \| annotate

isabelle

RSS Atom