isabelle: File revisions

src/HOL/Wellfounded.thy

2010-09-13	nipkow	2010-09-13	renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI	file \| diff \| annotate
2010-07-12	haftmann	2010-07-12	dropped superfluous [code del]s	file \| diff \| annotate
2010-06-11	haftmann	2010-06-11	declare lex_prod_def [code del]	file \| diff \| annotate
2010-05-05	krauss	2010-05-05	repaired comments where SOMEthing went utterly wrong (cf. 2b04504fcb69)	file \| diff \| annotate
2010-05-04	haftmann	2010-05-04	locale predicates of classes carry a mandatory "class" prefix	file \| diff \| annotate
2010-03-18	blanchet	2010-03-18	now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"	file \| diff \| annotate
2010-03-11	haftmann	2010-03-11	Big_Operators now in Main rather than Plain	file \| diff \| annotate
2010-03-10	haftmann	2010-03-10	split off theory Big_Operators from theory Finite_Set	file \| diff \| annotate
2010-02-18	huffman	2010-02-18	get rid of many duplicate simp rule warnings	file \| diff \| annotate
2009-10-26	krauss	2009-10-26	authentic constants; moved "acyclic" further down	file \| diff \| annotate
2009-10-26	krauss	2009-10-26	point-free characterization of well-foundedness	file \| diff \| annotate
2009-10-26	krauss	2009-10-26	replaced (outdated) comments by explicit statements	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-23	haftmann	2009-09-23	simplified proof	file \| diff \| annotate
2009-08-31	krauss	2009-08-31	moved lemma Wellfounded.in_inv_image to Relation.thy	file \| diff \| annotate
2009-08-31	krauss	2009-08-31	moved wfrec to Recdef.thy	file \| diff \| annotate
2009-08-31	krauss	2009-08-31	no consts_code for wfrec, as it violates the "code generation = equational reasoning" principle	file \| diff \| annotate
2009-07-28	haftmann	2009-07-28	explicit is better than implicit	file \| diff \| annotate
2009-07-28	krauss	2009-07-28	moved obsolete same_fst to Recdef.thy	file \| diff \| annotate
2009-07-27	krauss	2009-07-27	"more standard" argument order of relation composition (op O)	file \| diff \| annotate
2009-07-25	haftmann	2009-07-25	explicit is better than implicit	file \| diff \| annotate
2009-06-23	haftmann	2009-06-23	uniformly capitialized names for subdirectories	file \| diff \| annotate
2009-04-26	haftmann	2009-04-26	reverted slip in theory imports	file \| diff \| annotate
2009-04-26	haftmann	2009-04-26	adjusted to changes in power syntax	file \| diff \| annotate
2009-03-11	haftmann	2009-03-11	explicit code equations for some rarely used pred operations	file \| diff \| annotate
2009-01-21	haftmann	2009-01-21	changed import hierarchy	file \| diff \| annotate
2009-01-21	haftmann	2009-01-21	dropped ID	file \| diff \| annotate
2008-12-16	krauss	2008-12-16	method "sizechange" proves termination of functions; added more infrastructure for termination proofs	file \| diff \| annotate
2008-11-18	krauss	2008-11-18	removed lemmas called lemma1 and lemma2	file \| diff \| annotate
2008-11-12	krauss	2008-11-12	min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf	file \| diff \| annotate
2008-10-10	haftmann	2008-10-10	`code func` now just `code`	file \| diff \| annotate
2008-10-07	haftmann	2008-10-07	arbitrary is undefined	file \| diff \| annotate
2008-09-17	krauss	2008-09-17	wf_finite_psubset[simp], in_finite_psubset[simp]	file \| diff \| annotate
2008-08-11	haftmann	2008-08-11	moved class wellorder to theory Orderings	file \| diff \| annotate
2008-05-23	krauss	2008-05-23	rearranged subsections	file \| diff \| annotate
2008-05-07	berghofe	2008-05-07	- Explicitely passed pred_subset_eq and pred_equals_eq as an argument to the to_set and to_pred attributes, because it is no longer applied automatically - Manually applied predicate1I in proof of accp_subset, because it is no longer part of the claset - Replaced psubset_def by less_le	file \| diff \| annotate
2008-04-25	krauss	2008-04-25	Merged theories about wellfoundedness into one: Wellfounded.thy	file \| diff \| annotate

isabelle

RSS Atom