summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files | gz |
help

(0) -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip

(0) -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip

IntRingDefs is now redundant

new type class "zero" so that 0 can be overloaded

finally sum_below is overloaded properly

Multisets have a zero: the empty multiset

defining 0::int to be (int 0)

Now that 0 is overloaded, constant "zero" and its type class "zero" are
no longer needed. Also IntRingDefs is redundant

added type constraint ::nat because 0 is now overloaded

theory file NatSum.thy no longer needed
new files for the Allocator: AllocBase.{thy,ML}

theory file NatSum.thy no longer needed

Sums of geometric series