isabelle: Changelog

hoelzl [Tue, 12 Nov 2013 19:28:55 +0100] rev 54415

enat is countable

hoelzl [Tue, 12 Nov 2013 19:28:54 +0100] rev 54414

add equalities for SUP and INF over constant functions

hoelzl [Tue, 12 Nov 2013 19:28:54 +0100] rev 54413

add finite_select_induct; move generic lemmas from MV_Analysis/Linear_Algebra to the HOL image

hoelzl [Tue, 12 Nov 2013 19:28:53 +0100] rev 54412

add acyclicI_order

hoelzl [Tue, 12 Nov 2013 19:28:52 +0100] rev 54411

stronger inc_induct and dec_induct

hoelzl [Tue, 12 Nov 2013 19:28:51 +0100] rev 54410

countability of the image of a reflexive transitive closure

hoelzl [Tue, 12 Nov 2013 19:28:51 +0100] rev 54409

support of_rat with 0 or 1 on order relations

hoelzl [Tue, 12 Nov 2013 19:28:50 +0100] rev 54408

equation when indicator function equals 0 or 1

blanchet [Tue, 12 Nov 2013 14:24:34 +0100] rev 54407

ported part of function package to new 'Ctr_Sugar' abstraction

blanchet [Tue, 12 Nov 2013 14:00:56 +0100] rev 54406

undid copy-paste

isabelle