isabelle: File revisions

src/HOLCF/ConvexPD.thy

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
2009-03-26	wenzelm	2009-03-26	interpretation/interpret: prefixes are mandatory by default;	file \| diff \| annotate
2009-02-19	huffman	2009-02-19	avoid using ab_semigroup_idem_mult locale for powerdomains	file \| diff \| annotate
2009-01-29	nipkow	2009-01-29	commented out unused lemmas. May need to be put back by Brian.	file \| diff \| annotate
2009-01-16	haftmann	2009-01-16	migrated class package to new locale implementation	file \| diff \| annotate
2008-12-30	ballarin	2008-12-30	Merged.	file \| diff \| annotate
2008-12-19	ballarin	2008-12-19	More porting to new locales.	file \| diff \| annotate
2008-12-16	ballarin	2008-12-16	More porting to new locales.	file \| diff \| annotate
2008-12-16	huffman	2008-12-16	remove cvs Id tags	file \| diff \| annotate
2008-07-01	huffman	2008-07-01	rename approx_pd to pd_take	file \| diff \| annotate
2008-06-26	huffman	2008-06-26	remove cset theory; define ideal completions using typedef instead of cpodef	file \| diff \| annotate
2008-06-20	huffman	2008-06-20	simplify profinite class axioms	file \| diff \| annotate
2008-06-20	huffman	2008-06-20	clean up and rename some profinite lemmas	file \| diff \| annotate
2008-06-20	huffman	2008-06-20	removed SetPcpo.thy and cpo instance for type bool; added Cset.thy with pcpo type 'a cset isomorphic to 'a set; updated ideal completion theory to use cset	file \| diff \| annotate
2008-06-19	huffman	2008-06-19	move lemmas into locales; restructure some proofs	file \| diff \| annotate
2008-06-18	huffman	2008-06-18	add lemma compact_imp_principal to locale ideal_completion	file \| diff \| annotate
2008-05-19	huffman	2008-05-19	use new class package for classes profinite, bifinite; remove approx class	file \| diff \| annotate
2008-05-16	huffman	2008-05-16	rename locales; add completion_approx constant to ideal_completion locale; add new set-like syntax for powerdomains; reorganized proofs	file \| diff \| annotate
2008-05-07	berghofe	2008-05-07	Adapted to encoding of sets as predicates	file \| diff \| annotate
2008-03-27	huffman	2008-03-27	make preorder locale into a superclass of class po	file \| diff \| annotate
2008-03-26	huffman	2008-03-26	rename class bifinite_cpo to profinite; generalize powerdomains from bifinite to profinite	file \| diff \| annotate
2008-02-06	haftmann	2008-02-06	locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder	file \| diff \| annotate
2008-01-18	huffman	2008-01-18	change lemma admD to rule_format	file \| diff \| annotate
2008-01-14	huffman	2008-01-14	new theory of powerdomains	file \| diff \| annotate

isabelle

RSS Atom