isabelle: File revisions

Mercurial Mercurial > repos > isabelle / file revisions

src/ZF/QPair.ML

2000-09-07	wenzelm	tuned ML code (the_context, bind_thms(s));	file \| diff \| annotate
2000-06-30	paulson	removal of batch-style proofs	file \| diff \| annotate
2000-06-28	paulson	tidying and unbatchifying	file \| diff \| annotate
2000-03-22	paulson	tidied using new "inst" rule	file \| diff \| annotate
1999-01-13	paulson	datatype package improvements	file \| diff \| annotate
1998-09-18	paulson	tidied	file \| diff \| annotate
1998-08-06	paulson	even more tidying of Goal commands	file \| diff \| annotate
1998-07-15	paulson	More tidying and removal of "\!\!... from Goal commands	file \| diff \| annotate
1998-07-13	paulson	Huge tidy-up: removal of leading \!\!	file \| diff \| annotate
1998-06-22	wenzelm	isatool fixgoal;	file \| diff \| annotate
1997-12-24	paulson	New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort	file \| diff \| annotate
1997-11-03	wenzelm	isatool fixclasimp;	file \| diff \| annotate
1997-10-10	wenzelm	fixed dots;	file \| diff \| annotate
1997-04-23	paulson	Conversion to use blast_tac	file \| diff \| annotate
1997-01-08	paulson	Removal of sum_cs and eq_cs	file \| diff \| annotate
1997-01-03	paulson	Implicit simpsets and clasets for FOL and ZF	file \| diff \| annotate
1996-01-30	clasohm	expanded tabs	file \| diff \| annotate
1995-05-03	lcp	Modified proofs for (q)split, fst, snd for new	file \| diff \| annotate
1994-12-15	lcp	qconverse_qconverse, qconverse_prod: renamed from	file \| diff \| annotate
1994-12-14	clasohm	added bind_thm for theorems defined by "standard ..."	file \| diff \| annotate
1994-12-07	clasohm	added qed and qed_goal[w]	file \| diff \| annotate
1994-11-24	lcp	tidied proofs, using fast_tac etc. as much as possible	file \| diff \| annotate
1994-08-12	lcp	installation of new inductive/datatype sections	file \| diff \| annotate
1993-10-15	lcp	ZF/ind-syntax/refl_thin: new	file \| diff \| annotate
1993-09-17	lcp	Installation of new simplifier for ZF. Deleted all congruence rules not	file \| diff \| annotate
1993-09-16	clasohm	Initial revision	file \| diff \| annotate

less more (0) tip

isabelle

RSS Atom