isabelle: File revisions

src/HOLCF/Pcpodef.thy

2010-03-22	huffman	2010-03-22	remove LaTeX hyperref warnings by avoiding antiquotations within section headings	file \| diff \| annotate
2009-06-21	haftmann	2009-06-21	discontinued ancient tradition to suffix certain ML module names with "_package"	file \| diff \| annotate
2009-05-08	huffman	2009-05-08	rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names	file \| diff \| annotate
2008-12-16	huffman	2008-12-16	remove cvs Id tags	file \| diff \| annotate
2008-09-02	haftmann	2008-09-02	adapted to class instantiation compliance	file \| diff \| annotate
2008-06-20	huffman	2008-06-20	moved Abs_image to Typedef.thy; prove finite_UNIV outside the locale	file \| diff \| annotate
2008-03-27	huffman	2008-03-27	make preorder locale into a superclass of class po	file \| diff \| annotate
2008-01-31	huffman	2008-01-31	add lemma cpo_lubI	file \| diff \| annotate
2008-01-18	huffman	2008-01-18	pcpodef generates strict_iff lemmas	file \| diff \| annotate
2008-01-18	huffman	2008-01-18	change lemma admD to rule_format	file \| diff \| annotate
2008-01-17	huffman	2008-01-17	change class axiom chfin to rule_format	file \| diff \| annotate
2008-01-04	huffman	2008-01-04	new instance proofs for classes finite_po, chfin, flat	file \| diff \| annotate
2007-05-31	wenzelm	2007-05-31	moved HOLCF tools to canonical place;	file \| diff \| annotate
2006-05-01	huffman	2006-05-01	add theorem typdef_flat	file \| diff \| annotate
2005-10-11	huffman	2005-10-11	added theorem typedef_compact	file \| diff \| annotate
2005-10-10	huffman	2005-10-10	added theorem typedef_chfin	file \| diff \| annotate
2005-07-26	huffman	2005-07-26	cleaned up; renamed some theorems	file \| diff \| annotate
2005-07-07	huffman	2005-07-07	use theorems ch2ch_cont, cont2contlubE	file \| diff \| annotate
2005-07-06	huffman	2005-07-06	renamed from TypedefPcpo.thy; added theorems Rep_defined, Abs_defined; uses pcpodef_package.ML	file \| diff \| annotate

isabelle

RSS Atom