src/HOL/Library/Finite_Map.thy
18 months ago wenzelm 2018-03-07 more abbrevs -- this makes "(=" ambiguous and thus simplifies input of "(=)" (within the context of Main HOL);
20 months ago Lars Hupel 2018-01-22 repair malformed fundef_cong rule
20 months ago nipkow 2018-01-10 ran isabelle update_op on all sources
2017-08-11 Lars Hupel 2017-08-11 fmap :: size
2017-07-20 Lars Hupel 2017-07-20 tuned code setup
2017-07-16 Lars Hupel 2017-07-16 fmap is finite
2017-07-12 Lars Hupel 2017-07-12 more material on finite maps
2017-07-12 traytel 2017-07-12 redundant since c6714a9562ae
2017-07-11 Lars Hupel 2017-07-11 more material on fmaps
2017-07-11 Lars Hupel 2017-07-11 canonical representation for fmaps is fmlookup
2017-07-11 Lars Hupel 2017-07-11 fmaps are countable
2016-10-17 nipkow 2016-10-17 setsum -> sum
2016-10-13 Lars Hupel 2016-10-13 renamed lemma to a more consistent name
2016-10-13 Lars Hupel 2016-10-13 tuned
2016-10-13 Lars Hupel 2016-10-13 remove accidentally oops'ed (and wrong) lemma
2016-09-16 Lars Hupel 2016-09-16 tuned proofs
2016-09-15 Lars Hupel 2016-09-15 new type for finite maps; use it in HOL-Probability