isabelle: Changelog

Mercurial Mercurial > repos > isabelle / changelog

summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
(0) -30000 -10000 -3000 -1000 -300 -100 -30 -10 -6 +6 +10 +30 +100 +300 +1000 +3000 +10000 +30000 tip

Wed, 10 Oct 2012 10:48:33 +0200 special code setup for step function in IMP is redundant as definition was tuned (cf. c54d901d2946)

bulwahn [Wed, 10 Oct 2012 10:48:33 +0200] rev 49767

special code setup for step function in IMP is redundant as definition was tuned (cf. c54d901d2946)

Wed, 10 Oct 2012 10:48:17 +0200 test case for set_comprehension_pointfree simproc succeeds now

bulwahn [Wed, 10 Oct 2012 10:48:17 +0200] rev 49766

test case for set_comprehension_pointfree simproc succeeds now

Wed, 10 Oct 2012 10:47:52 +0200 unfolding bounded existential quantifiers as first step in the set_comprehension_pointfree simproc

bulwahn [Wed, 10 Oct 2012 10:47:52 +0200] rev 49765

unfolding bounded existential quantifiers as first step in the set_comprehension_pointfree simproc

Wed, 10 Oct 2012 10:47:43 +0200 moving simproc from Finite_Set to more appropriate Product_Type theory

bulwahn [Wed, 10 Oct 2012 10:47:43 +0200] rev 49764

moving simproc from Finite_Set to more appropriate Product_Type theory

Wed, 10 Oct 2012 10:47:21 +0200 generalizing set_comprehension_pointfree simproc to work for arbitrary predicates (and not just the finite predicate)

bulwahn [Wed, 10 Oct 2012 10:47:21 +0200] rev 49763

generalizing set_comprehension_pointfree simproc to work for arbitrary predicates (and not just the finite predicate)

Wed, 10 Oct 2012 10:41:18 +0200 adding some example that motivates some of the current changes in the set_comprehension_pointfree simproc

bulwahn [Wed, 10 Oct 2012 10:41:18 +0200] rev 49762

adding some example that motivates some of the current changes in the set_comprehension_pointfree simproc

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

isabelle