src/HOL/Library/Finite_Map.thy
12 months ago Lars Hupel 2018-06-18 material on finite sets and maps
12 months ago Lars Hupel 2018-06-18 simplify parametricity proofs
12 months ago nipkow 2018-06-06 Keep filter input syntax
13 months ago nipkow 2018-05-22 First step to remove nonstandard "[x <- xs. P]" syntax: only input
15 months ago wenzelm 2018-03-07 more abbrevs -- this makes "(=" ambiguous and thus simplifies input of "(=)" (within the context of Main HOL);
17 months ago Lars Hupel 2018-01-22 repair malformed fundef_cong rule
17 months ago nipkow 2018-01-10 ran isabelle update_op on all sources
22 months ago Lars Hupel 2017-08-11 fmap :: size
23 months ago Lars Hupel 2017-07-20 tuned code setup
23 months ago Lars Hupel 2017-07-16 fmap is finite
23 months ago Lars Hupel 2017-07-12 more material on finite maps
23 months ago traytel 2017-07-12 redundant since c6714a9562ae
23 months ago Lars Hupel 2017-07-11 more material on fmaps
23 months ago Lars Hupel 2017-07-11 canonical representation for fmaps is fmlookup
23 months ago 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