src/HOL/Library/Finite_Map.thy
8 months ago haftmann 2018-11-18 removed legacy input syntax
9 months ago Lars Hupel 2018-10-16 more material on finite maps
10 months ago Lars Hupel 2018-08-30 material on finite sets
11 months ago Lars Hupel 2018-08-25 material on finite maps
11 months ago Lars Hupel 2018-08-17 Finite_Map: monotonicity
13 months ago Lars Hupel 2018-06-18 material on finite sets and maps
13 months ago Lars Hupel 2018-06-18 simplify parametricity proofs
13 months ago nipkow 2018-06-06 Keep filter input syntax
14 months ago nipkow 2018-05-22 First step to remove nonstandard "[x <- xs. P]" syntax: only input
16 months ago wenzelm 2018-03-07 more abbrevs -- this makes "(=" ambiguous and thus simplifies input of "(=)" (within the context of Main HOL);
18 months ago Lars Hupel 2018-01-22 repair malformed fundef_cong rule
18 months ago nipkow 2018-01-10 ran isabelle update_op on all sources
23 months ago 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