Mercurial Mercurial > hg > nominal2 / changelog
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
(0) -1000 -300 -100 -60 +60 +100 +300 +1000 tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Tue, 23 Mar 2010 09:13:17 +0100 Move Let properties to ExLet
changeset
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 23 Mar 2010 09:13:17 +0100] rev 1602
Move Let properties to ExLet
Tue, 23 Mar 2010 09:06:28 +0100 Added missing file
changeset
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 23 Mar 2010 09:06:28 +0100] rev 1601
Added missing file
Tue, 23 Mar 2010 09:05:23 +0100 More reorganization.
changeset
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 23 Mar 2010 09:05:23 +0100] rev 1600
More reorganization.
Tue, 23 Mar 2010 08:51:43 +0100 Move Leroy out of Test, rename accordingly.
changeset
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 23 Mar 2010 08:51:43 +0100] rev 1599
Move Leroy out of Test, rename accordingly.
Tue, 23 Mar 2010 08:46:44 +0100 Term1 is identical to Example 3
changeset
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 23 Mar 2010 08:46:44 +0100] rev 1598
Term1 is identical to Example 3
Tue, 23 Mar 2010 08:45:08 +0100 Move example3 out.
changeset
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 23 Mar 2010 08:45:08 +0100] rev 1597
Move example3 out.
Tue, 23 Mar 2010 08:42:02 +0100 Move Ex1 and Ex2 out of Test
changeset
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 23 Mar 2010 08:42:02 +0100] rev 1596
Move Ex1 and Ex2 out of Test
Tue, 23 Mar 2010 08:33:48 +0100 Move examples which create more permutations out
changeset
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 23 Mar 2010 08:33:48 +0100] rev 1595
Move examples which create more permutations out
Tue, 23 Mar 2010 08:22:48 +0100 Move LamEx out of Test.
changeset
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 23 Mar 2010 08:22:48 +0100] rev 1594
Move LamEx out of Test.
Tue, 23 Mar 2010 08:20:13 +0100 Move lambda examples to manual
changeset
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 23 Mar 2010 08:20:13 +0100] rev 1593
Move lambda examples to manual
Tue, 23 Mar 2010 08:19:33 +0100 Move manual examples to a subdirectory.
changeset
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 23 Mar 2010 08:19:33 +0100] rev 1592
Move manual examples to a subdirectory.
Tue, 23 Mar 2010 08:16:39 +0100 Removed compat tests.
changeset
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 23 Mar 2010 08:16:39 +0100] rev 1591
Removed compat tests.
Tue, 23 Mar 2010 08:11:39 +0100 merge
changeset
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 23 Mar 2010 08:11:39 +0100] rev 1590
merge
Tue, 23 Mar 2010 08:11:11 +0100 Move Non-respectful examples to NotRsp
changeset
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 23 Mar 2010 08:11:11 +0100] rev 1589
Move Non-respectful examples to NotRsp
Tue, 23 Mar 2010 07:43:20 +0100 merged
changeset
Christian Urban <urbanc@in.tum.de> [Tue, 23 Mar 2010 07:43:20 +0100] rev 1588
merged
Tue, 23 Mar 2010 07:39:10 +0100 more on the paper
changeset
Christian Urban <urbanc@in.tum.de> [Tue, 23 Mar 2010 07:39:10 +0100] rev 1587
more on the paper
Tue, 23 Mar 2010 07:04:27 +0100 Move the comment to appropriate place.
changeset
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 23 Mar 2010 07:04:27 +0100] rev 1586
Move the comment to appropriate place.
Tue, 23 Mar 2010 07:04:14 +0100 Remove compose_eqvt
changeset
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 23 Mar 2010 07:04:14 +0100] rev 1585
Remove compose_eqvt
Mon, 22 Mar 2010 18:56:35 +0100 sym proof with compose.
changeset
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 22 Mar 2010 18:56:35 +0100] rev 1584
sym proof with compose.
Mon, 22 Mar 2010 18:38:59 +0100 Marked the place where a compose lemma applies.
changeset
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 22 Mar 2010 18:38:59 +0100] rev 1583
Marked the place where a compose lemma applies.
Mon, 22 Mar 2010 18:29:57 +0100 merge
changeset
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 22 Mar 2010 18:29:57 +0100] rev 1582
merge
Mon, 22 Mar 2010 18:29:29 +0100 equivp_cheat can be removed for all one-permutation examples.
changeset
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 22 Mar 2010 18:29:29 +0100] rev 1581
equivp_cheat can be removed for all one-permutation examples.
Mon, 22 Mar 2010 18:20:06 +0100 merged
changeset
Christian Urban <urbanc@in.tum.de> [Mon, 22 Mar 2010 18:20:06 +0100] rev 1580
merged
Mon, 22 Mar 2010 18:19:13 +0100 more on the paper
changeset
Christian Urban <urbanc@in.tum.de> [Mon, 22 Mar 2010 18:19:13 +0100] rev 1579
more on the paper
Mon, 22 Mar 2010 16:22:28 +0100 merged
changeset
Christian Urban <urbanc@in.tum.de> [Mon, 22 Mar 2010 16:22:28 +0100] rev 1578
merged
Mon, 22 Mar 2010 16:22:07 +0100 tuned paper
changeset
Christian Urban <urbanc@in.tum.de> [Mon, 22 Mar 2010 16:22:07 +0100] rev 1577
tuned paper
Mon, 22 Mar 2010 17:21:27 +0100 Got rid of alpha_bn_rsp_cheat.
changeset
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 22 Mar 2010 17:21:27 +0100] rev 1576
Got rid of alpha_bn_rsp_cheat.
Mon, 22 Mar 2010 15:27:01 +0100 alpha_bn_rsp_pre automatized.
changeset
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 22 Mar 2010 15:27:01 +0100] rev 1575
alpha_bn_rsp_pre automatized.
Mon, 22 Mar 2010 14:07:35 +0100 merge
changeset
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 22 Mar 2010 14:07:35 +0100] rev 1574
merge
Mon, 22 Mar 2010 14:07:07 +0100 fv_rsp proved automatically.
changeset
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 22 Mar 2010 14:07:07 +0100] rev 1573
fv_rsp proved automatically.
Mon, 22 Mar 2010 11:55:29 +0100 more on the paper
changeset
Christian Urban <urbanc@in.tum.de> [Mon, 22 Mar 2010 11:55:29 +0100] rev 1572
more on the paper
Mon, 22 Mar 2010 10:21:14 +0100 merged
changeset
Christian Urban <urbanc@in.tum.de> [Mon, 22 Mar 2010 10:21:14 +0100] rev 1571
merged
Mon, 22 Mar 2010 10:20:57 +0100 tuned paper
changeset
Christian Urban <urbanc@in.tum.de> [Mon, 22 Mar 2010 10:20:57 +0100] rev 1570
tuned paper
Mon, 22 Mar 2010 09:16:25 +0100 some tuning
changeset
Christian Urban <urbanc@in.tum.de> [Mon, 22 Mar 2010 09:16:25 +0100] rev 1569
some tuning
Mon, 22 Mar 2010 10:15:46 +0100 Strong induction for Type Schemes.
changeset
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 22 Mar 2010 10:15:46 +0100] rev 1568
Strong induction for Type Schemes.
Mon, 22 Mar 2010 09:02:30 +0100 Fixed missing colon.
changeset
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 22 Mar 2010 09:02:30 +0100] rev 1567
Fixed missing colon.
Sun, 21 Mar 2010 22:27:08 +0100 tuned paper
changeset
Christian Urban <urbanc@in.tum.de> [Sun, 21 Mar 2010 22:27:08 +0100] rev 1566
tuned paper
Sat, 20 Mar 2010 18:16:26 +0100 merged
changeset
Christian Urban <urbanc@in.tum.de> [Sat, 20 Mar 2010 18:16:26 +0100] rev 1565
merged
Sat, 20 Mar 2010 16:27:51 +0100 proved at_set_avoiding2 which is needed for strong induction principles
changeset
Christian Urban <urbanc@in.tum.de> [Sat, 20 Mar 2010 16:27:51 +0100] rev 1564
proved at_set_avoiding2 which is needed for strong induction principles
Sat, 20 Mar 2010 13:50:00 +0100 moved lemmas supp_perm_eq and exists_perm to Nominal2_Supp
changeset
Christian Urban <urbanc@in.tum.de> [Sat, 20 Mar 2010 13:50:00 +0100] rev 1563
moved lemmas supp_perm_eq and exists_perm to Nominal2_Supp
Sat, 20 Mar 2010 10:12:09 +0100 Size experiments.
changeset
Cezary Kaliszyk <kaliszyk@in.tum.de> [Sat, 20 Mar 2010 10:12:09 +0100] rev 1562
Size experiments.
Sat, 20 Mar 2010 09:27:28 +0100 Use 'alpha_bn_refl' to get rid of one of the sorrys.
changeset
Cezary Kaliszyk <kaliszyk@in.tum.de> [Sat, 20 Mar 2010 09:27:28 +0100] rev 1561
Use 'alpha_bn_refl' to get rid of one of the sorrys.
Sat, 20 Mar 2010 08:56:07 +0100 Build alpha-->alphabn implications
changeset
Cezary Kaliszyk <kaliszyk@in.tum.de> [Sat, 20 Mar 2010 08:56:07 +0100] rev 1560
Build alpha-->alphabn implications
Sat, 20 Mar 2010 08:04:59 +0100 Prove reflp for all relations.
changeset
Cezary Kaliszyk <kaliszyk@in.tum.de> [Sat, 20 Mar 2010 08:04:59 +0100] rev 1559
Prove reflp for all relations.
Sat, 20 Mar 2010 04:51:26 +0100 started cleaning up and introduced 3 versions of ~~gen
changeset
Christian Urban <urbanc@in.tum.de> [Sat, 20 Mar 2010 04:51:26 +0100] rev 1558
started cleaning up and introduced 3 versions of ~~gen
Sat, 20 Mar 2010 02:46:07 +0100 moved infinite_Un into mainstream Isabelle; moved permute_boolI/E lemmas
changeset
Christian Urban <urbanc@in.tum.de> [Sat, 20 Mar 2010 02:46:07 +0100] rev 1557
moved infinite_Un into mainstream Isabelle; moved permute_boolI/E lemmas
Fri, 19 Mar 2010 21:04:24 +0100 more work on the paper
changeset
Christian Urban <urbanc@in.tum.de> [Fri, 19 Mar 2010 21:04:24 +0100] rev 1556
more work on the paper
Fri, 19 Mar 2010 18:56:13 +0100 Described automatically created funs.
changeset
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 19 Mar 2010 18:56:13 +0100] rev 1555
Described automatically created funs.
Fri, 19 Mar 2010 18:43:29 +0100 merge
changeset
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 19 Mar 2010 18:43:29 +0100] rev 1554
merge
Fri, 19 Mar 2010 18:42:57 +0100 Automatically derive support for datatypes with at-most one binding per constructor.
changeset
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 19 Mar 2010 18:42:57 +0100] rev 1553
Automatically derive support for datatypes with at-most one binding per constructor.
Fri, 19 Mar 2010 17:20:25 +0100 picture
changeset
Christian Urban <urbanc@in.tum.de> [Fri, 19 Mar 2010 17:20:25 +0100] rev 1552
picture
Fri, 19 Mar 2010 15:43:59 +0100 merged
changeset
Christian Urban <urbanc@in.tum.de> [Fri, 19 Mar 2010 15:43:59 +0100] rev 1551
merged
Fri, 19 Mar 2010 15:43:43 +0100 polished
changeset
Christian Urban <urbanc@in.tum.de> [Fri, 19 Mar 2010 15:43:43 +0100] rev 1550
polished
Fri, 19 Mar 2010 15:01:01 +0100 Update Test to use fset.
changeset
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 19 Mar 2010 15:01:01 +0100] rev 1549
Update Test to use fset.
Fri, 19 Mar 2010 14:54:57 +0100 merge
changeset
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 19 Mar 2010 14:54:57 +0100] rev 1548
merge
Fri, 19 Mar 2010 14:54:30 +0100 Use fs typeclass in showing finite support + some cheat cleaning.
changeset
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 19 Mar 2010 14:54:30 +0100] rev 1547
Use fs typeclass in showing finite support + some cheat cleaning.
Fri, 19 Mar 2010 12:31:55 +0100 merged
changeset
Christian Urban <urbanc@in.tum.de> [Fri, 19 Mar 2010 12:31:55 +0100] rev 1546
merged
Fri, 19 Mar 2010 12:31:17 +0100 more one the paper
changeset
Christian Urban <urbanc@in.tum.de> [Fri, 19 Mar 2010 12:31:17 +0100] rev 1545
more one the paper
Fri, 19 Mar 2010 12:28:35 +0100 Keep only one copy of infinite_Un.
changeset
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 19 Mar 2010 12:28:35 +0100] rev 1544
Keep only one copy of infinite_Un.
Fri, 19 Mar 2010 12:24:16 +0100 Added a missing 'import'.
changeset
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 19 Mar 2010 12:24:16 +0100] rev 1543
Added a missing 'import'.
(0) -1000 -300 -100 -60 +60 +100 +300 +1000 tip
nominal2