isabelle: File revisions

src/HOL/Library/RBT.thy

2012-10-12	wenzelm	2012-10-12	discontinued obsolete typedef (open) syntax;	file \| diff \| annotate
2012-07-31	kuncar	2012-07-31	use lifting/transfer formalization of RBT from Lift_RBT	file \| diff \| annotate
2012-04-13	Andreas Lochbihler	2012-04-13	move RBT implementation into type class contexts	file \| diff \| annotate
2012-02-21	bulwahn	2012-02-21	subtype preprocessing in Quickcheck; adding option use_subtype; tuned	file \| diff \| annotate
2012-01-06	haftmann	2012-01-06	incorporated canonical fold combinator on lists into body of List theory; refactored passages on List.fold(l/r)	file \| diff \| annotate
2011-12-20	bulwahn	2011-12-20	adding quickcheck generators in some HOL-Library theories	file \| diff \| annotate
2011-11-30	wenzelm	2011-11-30	prefer typedef without extra definition and alternative name; tuned proofs;	file \| diff \| annotate
2011-06-01	bulwahn	2011-06-01	splitting RBT theory into RBT and RBT_Mapping	file \| diff \| annotate
2010-11-18	haftmann	2010-11-18	proper qualification needed due to shadowing on theory merge	file \| diff \| annotate
2010-09-13	haftmann	2010-09-13	*established emerging canonical names _eqI and _eq_iff*	file \| diff \| annotate
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-09-07	nipkow	2010-09-07	expand_fun_eq -> ext_iff expand_set_eq -> set_ext_iff Naming in line now with multisets	file \| diff \| annotate
2010-08-27	haftmann	2010-08-27	renamed class/constant eq to equal; tuned some instantiations	file \| diff \| annotate
2010-06-18	haftmann	2010-06-18	prefer fold over foldl	file \| diff \| annotate
2010-05-21	haftmann	2010-05-21	tuned	file \| diff \| annotate
2010-05-20	haftmann	2010-05-20	implement Mapping.map_entry	file \| diff \| annotate
2010-04-21	hoelzl	2010-04-21	merged	file \| diff \| annotate
2010-04-16	wenzelm	2010-04-16	replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;	file \| diff \| annotate
2010-04-15	haftmann	2010-04-15	theory RBT with abstract type of red-black trees backed by implementation RBT_Impl	file \| diff \| annotate \| base
2010-03-06	haftmann	2010-03-06	some lemma refinements	file \| diff \| annotate
2010-03-06	haftmann	2010-03-06	added bulkload; tuned document	file \| diff \| annotate
2010-03-05	haftmann	2010-03-05	moved lemma map_sorted_distinct_set_unique	file \| diff \| annotate
2010-03-05	haftmann	2010-03-05	various refinements	file \| diff \| annotate
2010-03-03	haftmann	2010-03-03	restructured RBT theory	file \| diff \| annotate
2010-03-03	haftmann	2010-03-03	more explicit naming scheme	file \| diff \| annotate
2009-07-28	krauss	2009-07-28	tuned	file \| diff \| annotate
2009-07-27	krauss	2009-07-27	added missing proof of RBT.map_of_alist_of (contributed by Peter Lammich)	file \| diff \| annotate
2009-03-27	haftmann	2009-03-27	normalized imports	file \| diff \| annotate
2009-03-04	nipkow	2009-03-04	Made Option a separate theory and renamed option_map to Option.map	file \| diff \| annotate
2008-06-26	haftmann	2008-06-26	established Plain theory and image	file \| diff \| annotate
2008-03-03	krauss	2008-03-03	new theory of red-black trees, an efficient implementation of finite maps.	file \| diff \| annotate

isabelle

RSS Atom