isabelle: File revisions

src/HOL/Library/Multiset.thy

2015-07-18	wenzelm	2015-07-18	prefer tactics with explicit context;	file \| diff \| annotate
2015-07-06	wenzelm	2015-07-06	tuned proofs;	file \| diff \| annotate
2015-06-30	hoelzl	2015-06-30	fix tex-output for rel_mset	file \| diff \| annotate
2015-06-29	wenzelm	2015-06-29	tuned proofs;	file \| diff \| annotate
2015-06-29	wenzelm	2015-06-29	more symbols;	file \| diff \| annotate
2015-06-29	wenzelm	2015-06-29	more symbols; tuned proofs; tuned ML;	file \| diff \| annotate
2015-06-19	nipkow	2015-06-19	renamed multiset_of -> mset	file \| diff \| annotate
2015-06-18	nipkow	2015-06-18	multiset_of_set -> mset_set	file \| diff \| annotate
2015-06-17	wenzelm	2015-06-17	merged	file \| diff \| annotate
2015-06-17	wenzelm	2015-06-17	manual merge;	file \| diff \| annotate
2015-06-17	wenzelm	2015-06-17	isabelle update_cartouches;	file \| diff \| annotate
2015-06-17	nipkow	2015-06-17	more compact name	file \| diff \| annotate
2015-06-17	nipkow	2015-06-17	renamed Multiset.set_of to the canonical set_mset	file \| diff \| annotate
2015-06-10	fleury	2015-06-10	tuned	file \| diff \| annotate
2015-06-10	Mathias Fleury	2015-06-10	Renaming multiset operators < ~> <#,...	file \| diff \| annotate
2015-04-10	nipkow	2015-04-10	merged	file \| diff \| annotate
2015-04-10	nipkow	2015-04-10	renamed Multiset.fold -> fold_mset, Multiset.filter -> filter_mset	file \| diff \| annotate
2015-04-10	wenzelm	2015-04-10	tuned proofs;	file \| diff \| annotate
2015-04-09	blanchet	2015-04-09	introduced new abbreviations for multiset operations (in the hope of getting rid of the old names <, <=, etc.)	file \| diff \| annotate
2015-04-08	blanchet	2015-04-08	renamed multiset ordering to free up nice <# etc. symbols for the standard subset	file \| diff \| annotate
2015-04-07	nipkow	2015-04-07	Removed mcard because it is equal to size	file \| diff \| annotate
2015-03-23	haftmann	2015-03-23	explicit commutative additive inverse operation; more explicit focal point for commutative monoids with an inverse operation	file \| diff \| annotate
2015-03-25	blanchet	2015-03-25	more multiset theorems	file \| diff \| annotate
2015-03-25	wenzelm	2015-03-25	prefer local fixes;	file \| diff \| annotate
2015-03-06	wenzelm	2015-03-06	proper context;	file \| diff \| annotate
2015-02-19	haftmann	2015-02-19	establish unique preferred fact names	file \| diff \| annotate
2014-11-02	wenzelm	2014-11-02	modernized header;	file \| diff \| annotate
2014-09-24	blanchet	2014-09-24	simpler proof	file \| diff \| annotate
2014-09-09	nipkow	2014-09-09	enamed drop_Suc_conv_tl and nth_drop' to Cons_nth_drop_Suc	file \| diff \| annotate
2014-08-30	haftmann	2014-08-30	inlined unused definition	file \| diff \| annotate
2014-08-22	blanchet	2014-08-22	added lemmas contributed by Rene Thiemann	file \| diff \| annotate
2014-08-17	blanchet	2014-08-17	use 'image_mset' as BNF map function	file \| diff \| annotate
2014-07-05	haftmann	2014-07-05	refrain from auxiliary abbreviation: be more explicit to the reader in situations where syntax translation does not apply; uniform appearance of xsymbol and HTML output for sums	file \| diff \| annotate
2014-07-05	haftmann	2014-07-05	prefer ac_simps collections over separate name bindings for add and mult	file \| diff \| annotate
2014-07-04	haftmann	2014-07-04	reduced name variants for assoc and commute on plus and mult	file \| diff \| annotate
2014-06-11	Thomas Sewell	2014-06-11	Hypsubst preserves equality hypotheses Fixes included for various theories affected by this change.	file \| diff \| annotate
2014-06-28	haftmann	2014-06-28	fact consolidation	file \| diff \| annotate
2014-04-23	blanchet	2014-04-23	size function for multisets	file \| diff \| annotate
2014-03-06	blanchet	2014-03-06	renamed 'fun_rel' to 'rel_fun'	file \| diff \| annotate
2014-03-05	wenzelm	2014-03-05	proper UTF-8;	file \| diff \| annotate
2014-02-28	traytel	2014-02-28	load Metis a little later	file \| diff \| annotate
2014-02-28	nipkow	2014-02-28	added Rene Thiemann's patch for the nonterminating equality/subset test code for multisets	file \| diff \| annotate
2014-02-18	kuncar	2014-02-18	simplify proofs because of the stronger reflexivity prover	file \| diff \| annotate
2014-02-14	blanchet	2014-02-14	renamed 'enriched_type' to more informative 'functor' (following the renaming of enriched type constructors to bounded natural functors)	file \| diff \| annotate
2014-02-12	blanchet	2014-02-12	adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems * * * more transition of 'xxx_rec' to 'rec_xxx' and same for case * * * compile * * * 'rename_tac's to avoid referring to generated names * * * more robust scripts with 'rename_tac' * * * 'where' -> 'of' * * * 'where' -> 'of' * * * renamed 'xxx_rec' to 'rec_xxx'	file \| diff \| annotate
2014-01-24	blanchet	2014-01-24	killed 'More_BNFs' by moving its various bits where they (now) belong	file \| diff \| annotate
2013-12-27	haftmann	2013-12-27	prefer target-style syntaxx for sublocale	file \| diff \| annotate
2013-11-10	haftmann	2013-11-10	qualifed popular user space names	file \| diff \| annotate
2013-06-02	haftmann	2013-06-02	type class for confined subtraction	file \| diff \| annotate
2013-04-04	haftmann	2013-04-04	sup on multisets	file \| diff \| annotate
2013-04-03	haftmann	2013-04-03	default implementation of multisets by list with reasonable coverage of operations on multisets	file \| diff \| annotate
2013-04-03	haftmann	2013-04-03	optionalized very specific code setup for multisets	file \| diff \| annotate
2013-03-27	haftmann	2013-03-27	centralized various multiset operations in theory multiset; more conversions between multisets and lists respectively	file \| diff \| annotate
2013-02-15	haftmann	2013-02-15	attempt to re-establish conventions which theories are loaded into the grand unified library theory; four different code generation tests for different code setup constellations; augment code generation setup where necessary	file \| diff \| annotate
2013-02-15	haftmann	2013-02-15	two target language numeral types: integer and natural, as replacement for code_numeral; former theory HOL/Library/Code_Numeral_Types replaces HOL/Code_Numeral; refined stack of theories implementing int and/or nat by target language numerals; reduced number of target language numeral types to exactly one	file \| diff \| annotate
2013-02-14	haftmann	2013-02-14	reform of predicate compiler / quickcheck theories: implement yieldn operations uniformly on the ML level -- predicate compiler uses negative integers as parameter to yieldn, whereas code_numeral represents natural numbers! avoid odd New_ prefix by joining related theories; avoid overcompact name DSequence; separated predicate inside random monad into separate theory; consolidated name of theory Quickcheck	file \| diff \| annotate
2012-10-12	wenzelm	2012-10-12	discontinued obsolete typedef (open) syntax;	file \| diff \| annotate
2012-10-11	haftmann	2012-10-11	avoid global interpretation	file \| diff \| annotate
2012-10-11	haftmann	2012-10-11	simplified construction of fold combinator on multisets; more coherent name for fold combinator on multisets	file \| diff \| annotate
2012-10-04	haftmann	2012-10-04	default simp rule for image under identity	file \| diff \| annotate

isabelle

RSS Atom