Mercurial Mercurial > repos > isabelle / changelog
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
(0) -30000 -10000 -3000 -1000 -300 -100 -50 -24 +24 +50 +100 +300 +1000 +3000 +10000 tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Wed, 13 Nov 2013 11:23:25 +0100 tuned example
changeset
traytel [Wed, 13 Nov 2013 11:23:25 +0100] rev 54423
tuned example
Wed, 13 Nov 2013 12:32:26 +0100 shortened generated property name
changeset
blanchet [Wed, 13 Nov 2013 12:32:26 +0100] rev 54422
shortened generated property name
Wed, 13 Nov 2013 10:53:36 +0100 more explicit syntax for defining a bnf
changeset
traytel [Wed, 13 Nov 2013 10:53:36 +0100] rev 54421
more explicit syntax for defining a bnf
Wed, 13 Nov 2013 09:37:00 +0100 fix document generation for HOL-Probability
changeset
hoelzl [Wed, 13 Nov 2013 09:37:00 +0100] rev 54420
fix document generation for HOL-Probability
Tue, 12 Nov 2013 20:08:29 +0100 fix document generation for Extended_Nat
changeset
hoelzl [Tue, 12 Nov 2013 20:08:29 +0100] rev 54419
fix document generation for Extended_Nat
Tue, 12 Nov 2013 19:28:56 +0100 measure of a countable union
changeset
hoelzl [Tue, 12 Nov 2013 19:28:56 +0100] rev 54418
measure of a countable union
Tue, 12 Nov 2013 19:28:56 +0100 add restrict_space measure
changeset
hoelzl [Tue, 12 Nov 2013 19:28:56 +0100] rev 54417
add restrict_space measure
Tue, 12 Nov 2013 19:28:55 +0100 better support for enat and ereal conversions
changeset
hoelzl [Tue, 12 Nov 2013 19:28:55 +0100] rev 54416
better support for enat and ereal conversions
Tue, 12 Nov 2013 19:28:55 +0100 enat is countable
changeset
hoelzl [Tue, 12 Nov 2013 19:28:55 +0100] rev 54415
enat is countable
Tue, 12 Nov 2013 19:28:54 +0100 add equalities for SUP and INF over constant functions
changeset
hoelzl [Tue, 12 Nov 2013 19:28:54 +0100] rev 54414
add equalities for SUP and INF over constant functions
Tue, 12 Nov 2013 19:28:54 +0100 add finite_select_induct; move generic lemmas from MV_Analysis/Linear_Algebra to the HOL image
changeset
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
Tue, 12 Nov 2013 19:28:53 +0100 add acyclicI_order
changeset
hoelzl [Tue, 12 Nov 2013 19:28:53 +0100] rev 54412
add acyclicI_order
Tue, 12 Nov 2013 19:28:52 +0100 stronger inc_induct and dec_induct
changeset
hoelzl [Tue, 12 Nov 2013 19:28:52 +0100] rev 54411
stronger inc_induct and dec_induct
Tue, 12 Nov 2013 19:28:51 +0100 countability of the image of a reflexive transitive closure
changeset
hoelzl [Tue, 12 Nov 2013 19:28:51 +0100] rev 54410
countability of the image of a reflexive transitive closure
Tue, 12 Nov 2013 19:28:51 +0100 support of_rat with 0 or 1 on order relations
changeset
hoelzl [Tue, 12 Nov 2013 19:28:51 +0100] rev 54409
support of_rat with 0 or 1 on order relations
Tue, 12 Nov 2013 19:28:50 +0100 equation when indicator function equals 0 or 1
changeset
hoelzl [Tue, 12 Nov 2013 19:28:50 +0100] rev 54408
equation when indicator function equals 0 or 1
Tue, 12 Nov 2013 14:24:34 +0100 ported part of function package to new 'Ctr_Sugar' abstraction
changeset
blanchet [Tue, 12 Nov 2013 14:24:34 +0100] rev 54407
ported part of function package to new 'Ctr_Sugar' abstraction
Tue, 12 Nov 2013 14:00:56 +0100 undid copy-paste
changeset
blanchet [Tue, 12 Nov 2013 14:00:56 +0100] rev 54406
undid copy-paste
Tue, 12 Nov 2013 13:47:24 +0100 ported 'partial_function' to 'Ctr_Sugar' abstraction
changeset
blanchet [Tue, 12 Nov 2013 13:47:24 +0100] rev 54405
ported 'partial_function' to 'Ctr_Sugar' abstraction
Tue, 12 Nov 2013 13:47:24 +0100 port list comprehension simproc to 'Ctr_Sugar' abstraction
changeset
blanchet [Tue, 12 Nov 2013 13:47:24 +0100] rev 54404
port list comprehension simproc to 'Ctr_Sugar' abstraction
Tue, 12 Nov 2013 13:47:24 +0100 added convenience function
changeset
blanchet [Tue, 12 Nov 2013 13:47:24 +0100] rev 54403
added convenience function
Tue, 12 Nov 2013 13:47:24 +0100 document idiomatic use of 'simps_of_case'
changeset
blanchet [Tue, 12 Nov 2013 13:47:24 +0100] rev 54402
document idiomatic use of 'simps_of_case'
Tue, 12 Nov 2013 13:47:24 +0100 ported 'Simps_Case_Conv' to use new 'Ctr_Sugar' abstraction
changeset
blanchet [Tue, 12 Nov 2013 13:47:24 +0100] rev 54401
ported 'Simps_Case_Conv' to use new 'Ctr_Sugar' abstraction
Tue, 12 Nov 2013 13:47:24 +0100 register old-style datatypes as 'Ctr_Sugar'
changeset
blanchet [Tue, 12 Nov 2013 13:47:24 +0100] rev 54400
register old-style datatypes as 'Ctr_Sugar'
(0) -30000 -10000 -3000 -1000 -300 -100 -50 -24 +24 +50 +100 +300 +1000 +3000 +10000 tip
isabelle