isabelle: File revisions

src/HOL/List.ML

2000-08-17	nipkow	2000-08-17	added map_cong to recdef	file \| diff \| annotate
2000-07-24	wenzelm	2000-07-24	avoid referencing thy value; rename_numerals: use implicit theory context;	file \| diff \| annotate
2000-07-14	paulson	2000-07-14	moved sublist from UNITY/AllocBase to List	file \| diff \| annotate
2000-07-06	nipkow	2000-07-06	Deleted list_case thms no subsumed by case_tac	file \| diff \| annotate
2000-06-29	paulson	2000-06-29	fixed proof to cope with the default of equalityCE instead of equalityE	file \| diff \| annotate
2000-06-22	wenzelm	2000-06-22	bind_thm(s);	file \| diff \| annotate
2000-06-01	paulson	2000-06-01	simplified the proof of nth_upt	file \| diff \| annotate
2000-05-31	paulson	2000-05-31	added new proofs and simplified an old one	file \| diff \| annotate
2000-05-26	paulson	2000-05-26	renamed upt_Suc, since that name is needed for its primrec rule	file \| diff \| annotate
2000-05-23	paulson	2000-05-23	added type constraint ::nat because 0 is now overloaded	file \| diff \| annotate
2000-04-19	paulson	2000-04-19	removal of less_SucI, le_SucI from default simpset	file \| diff \| annotate
2000-03-13	wenzelm	2000-03-13	case_tac now subsumes both boolean and datatype cases;	file \| diff \| annotate
2000-03-13	nipkow	2000-03-13	exhaust_tac -> cases_tac	file \| diff \| annotate
2000-02-24	nipkow	2000-02-24	Added and renamed a lemma.	file \| diff \| annotate
2000-02-18	paulson	2000-02-18	expandshort	file \| diff \| annotate
2000-01-26	nipkow	2000-01-26	optimized xs[i:=x]!j lemmas.	file \| diff \| annotate
2000-01-12	nipkow	2000-01-12	More lemmas.	file \| diff \| annotate
2000-01-10	nipkow	2000-01-10	Forgot to "call" MicroJava in makefile. Added list_all2 to List.	file \| diff \| annotate
1999-12-13	paulson	1999-12-13	expandshort	file \| diff \| annotate
1999-11-11	nipkow	1999-11-11	Imported Conny's lemmas from MicroJava	file \| diff \| annotate
1999-09-21	nipkow	1999-09-21	Mod because of new solver interface.	file \| diff \| annotate
1999-08-18	nipkow	1999-08-18	Added take_all and drop_all to simpset.	file \| diff \| annotate
1999-08-16	wenzelm	1999-08-16	'a list: Nil, Cons;	file \| diff \| annotate
1999-07-19	paulson	1999-07-19	NatBin: binary arithmetic for the naturals	file \| diff \| annotate
1999-07-18	nipkow	1999-07-18	Modifid length_tl	file \| diff \| annotate
1999-06-17	paulson	1999-06-17	expandshort	file \| diff \| annotate
1999-06-11	nipkow	1999-06-11	rev=rev lemma.	file \| diff \| annotate
1999-06-10	paulson	1999-06-10	many new lemmas about take & drop, incl the famous take-lemma Ran expandshort	file \| diff \| annotate
1999-06-07	nipkow	1999-06-07	Added lots of 'replicate' lemmas.	file \| diff \| annotate
1999-04-20	paulson	1999-04-20	tidied	file \| diff \| annotate
1999-04-15	nipkow	1999-04-15	Added new thms.	file \| diff \| annotate
1999-04-01	pusch	1999-04-01	new definition for nth. added warnings, if primrec definition is deleted from simpset.	file \| diff \| annotate
1999-03-17	wenzelm	1999-03-17	Theory.sign_of;	file \| diff \| annotate
1999-03-08	nipkow	1999-03-08	modified zip	file \| diff \| annotate
1999-01-29	paulson	1999-01-29	expandshort	file \| diff \| annotate
1999-01-19	paulson	1999-01-19	removal of the (thm list) argument of mk_cases	file \| diff \| annotate
1999-01-09	nipkow	1999-01-09	Refined arith tactic.	file \| diff \| annotate
1999-01-04	nipkow	1999-01-04	Shortened a proof.	file \| diff \| annotate
1999-01-04	nipkow	1999-01-04	Version 1.0 of linear nat arithmetic.	file \| diff \| annotate
1998-11-27	nipkow	1998-11-27	At last: linear arithmetic for nat!	file \| diff \| annotate
1998-10-23	oheimb	1998-10-23	corrected auto_tac (applications of unsafe wrappers)	file \| diff \| annotate
1998-10-14	nipkow	1998-10-14	Nat: added zero_neq_conv List: added nth/update lemmas.	file \| diff \| annotate
1998-10-13	paulson	1998-10-13	length_Suc_conv is no longer given to AddIffs	file \| diff \| annotate
1998-09-23	paulson	1998-09-23	deleted needless parentheses	file \| diff \| annotate
1998-09-21	oheimb	1998-09-21	re-added mem and list_all	file \| diff \| annotate
1998-09-10	paulson	1998-09-10	in_set_butlast_appendI supersedes in_set_butlast_appendI1,2	file \| diff \| annotate
1998-09-09	oheimb	1998-09-09	changed constants mem and list_all to mere translations added filter_is_subset	file \| diff \| annotate
1998-09-04	nipkow	1998-09-04	Arith: less_diff_conv List: [i..j]	file \| diff \| annotate
1998-09-02	nipkow	1998-09-02	Added function upto to List. Had to rearrange loading sequence because now List uses Recdef.	file \| diff \| annotate
1998-08-20	paulson	1998-08-20	tidied	file \| diff \| annotate
1998-08-14	paulson	1998-08-14	expandshort	file \| diff \| annotate
1998-08-13	paulson	1998-08-13	even more tidying of Goal commands	file \| diff \| annotate
1998-08-12	oheimb	1998-08-12	added length_Suc_conv, finite_set	file \| diff \| annotate
1998-08-10	nipkow	1998-08-10	More lemmas about lex.	file \| diff \| annotate
1998-08-08	nipkow	1998-08-08	List now contains some lexicographic orderings.	file \| diff \| annotate
1998-08-06	paulson	1998-08-06	even more tidying of Goal commands	file \| diff \| annotate
1998-08-06	nipkow	1998-08-06	New lemmas in List and Lambda in IsaMakefile	file \| diff \| annotate
1998-07-27	nipkow	1998-07-27	conversion bug in simpproc list_eq	file \| diff \| annotate
1998-07-24	berghofe	1998-07-24	Adapted to new datatype package.	file \| diff \| annotate
1998-07-20	nipkow	1998-07-20	Added simproc list_eq.	file \| diff \| annotate

isabelle

RSS Atom