nominal2: Changelog

Mercurial Mercurial > hg > nominal2 / changelog

Mon, 29 Mar 2010 16:44:05 +0200 merge

changeset

Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 29 Mar 2010 16:44:05 +0200] rev 1696

merge

Mon, 29 Mar 2010 16:29:50 +0200 Changed to Lists.

changeset

Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 29 Mar 2010 16:29:50 +0200] rev 1695

Changed to Lists.

Mon, 29 Mar 2010 16:41:21 +0200 clarified core-haskell example

changeset

Christian Urban <urbanc@in.tum.de> [Mon, 29 Mar 2010 16:41:21 +0200] rev 1694

clarified core-haskell example

Mon, 29 Mar 2010 14:58:00 +0200 spell check

changeset

Christian Urban <urbanc@in.tum.de> [Mon, 29 Mar 2010 14:58:00 +0200] rev 1693

spell check

Mon, 29 Mar 2010 12:06:22 +0200 merge

changeset

Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 29 Mar 2010 12:06:22 +0200] rev 1692

merge

Mon, 29 Mar 2010 12:06:05 +0200 Abs_gen and Abs_let simplifications.

changeset

Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 29 Mar 2010 12:06:05 +0200] rev 1691

Abs_gen and Abs_let simplifications.

Mon, 29 Mar 2010 11:23:29 +0200 more on the paper

changeset

Christian Urban <urbanc@in.tum.de> [Mon, 29 Mar 2010 11:23:29 +0200] rev 1690

more on the paper

Sun, 28 Mar 2010 22:54:38 +0200 got rid of the aux-function on the raw level, by defining it with function on the quotient level

changeset

Christian Urban <urbanc@in.tum.de> [Sun, 28 Mar 2010 22:54:38 +0200] rev 1686

got rid of the aux-function on the raw level, by defining it with function on the quotient level

Sat, 27 Mar 2010 16:20:39 +0100 Lets finally abstract lists.

changeset

Cezary Kaliszyk <kaliszyk@in.tum.de> [Sat, 27 Mar 2010 16:20:39 +0100] rev 1685

Lets finally abstract lists.

Sat, 27 Mar 2010 16:17:45 +0100 Core Haskell can now use proper strings.

changeset

Cezary Kaliszyk <kaliszyk@in.tum.de> [Sat, 27 Mar 2010 16:17:45 +0100] rev 1684

Core Haskell can now use proper strings.

Sat, 27 Mar 2010 14:55:07 +0100 Automatically lift theorems and constants only using the new quotient types. Requires new Isabelle.

changeset

Cezary Kaliszyk <kaliszyk@in.tum.de> [Sat, 27 Mar 2010 14:55:07 +0100] rev 1683

Automatically lift theorems and constants only using the new quotient types. Requires new Isabelle.

Sat, 27 Mar 2010 14:38:22 +0100 Remove list_eq notation.

changeset

Cezary Kaliszyk <kaliszyk@in.tum.de> [Sat, 27 Mar 2010 14:38:22 +0100] rev 1682

Remove list_eq notation.

Sat, 27 Mar 2010 13:50:59 +0100 Get lifted types information from the quotient package.

changeset

Cezary Kaliszyk <kaliszyk@in.tum.de> [Sat, 27 Mar 2010 13:50:59 +0100] rev 1681

Get lifted types information from the quotient package.

Sat, 27 Mar 2010 12:26:59 +0100 Equivariance when bn functions are lists.

changeset

Cezary Kaliszyk <kaliszyk@in.tum.de> [Sat, 27 Mar 2010 12:26:59 +0100] rev 1680

Equivariance when bn functions are lists.

Sat, 27 Mar 2010 12:20:17 +0100 Accepts lists in FV.

changeset

Cezary Kaliszyk <kaliszyk@in.tum.de> [Sat, 27 Mar 2010 12:20:17 +0100] rev 1679

Accepts lists in FV.

Sat, 27 Mar 2010 12:01:28 +0100 Parsing of list-bn functions into components.

changeset

Cezary Kaliszyk <kaliszyk@in.tum.de> [Sat, 27 Mar 2010 12:01:28 +0100] rev 1678

Parsing of list-bn functions into components.

Sat, 27 Mar 2010 09:56:35 +0100 Automatically compute support if only one type of Abs is present in the type.

changeset

Cezary Kaliszyk <kaliszyk@in.tum.de> [Sat, 27 Mar 2010 09:56:35 +0100] rev 1677

Automatically compute support if only one type of Abs is present in the type.

Sat, 27 Mar 2010 09:41:00 +0100 Manually proved TySch support; All properties of TySch now true.

changeset

Cezary Kaliszyk <kaliszyk@in.tum.de> [Sat, 27 Mar 2010 09:41:00 +0100] rev 1676

Manually proved TySch support; All properties of TySch now true.

Sat, 27 Mar 2010 09:21:43 +0100 Generalize Abs_eq_iff.

changeset

Cezary Kaliszyk <kaliszyk@in.tum.de> [Sat, 27 Mar 2010 09:21:43 +0100] rev 1675

Generalize Abs_eq_iff.

Sat, 27 Mar 2010 09:15:09 +0100 Minor fix.

changeset

Cezary Kaliszyk <kaliszyk@in.tum.de> [Sat, 27 Mar 2010 09:15:09 +0100] rev 1674

Minor fix.

Sat, 27 Mar 2010 08:42:07 +0100 New compose lemmas. Reverted alpha_gen sym/trans changes. Equivp for alpha_res should work now.

changeset

Cezary Kaliszyk <kaliszyk@in.tum.de> [Sat, 27 Mar 2010 08:42:07 +0100] rev 1673

New compose lemmas. Reverted alpha_gen sym/trans changes. Equivp for alpha_res should work now.

Sat, 27 Mar 2010 08:17:43 +0100 Initial proof modifications for alpha_res

changeset

Cezary Kaliszyk <kaliszyk@in.tum.de> [Sat, 27 Mar 2010 08:17:43 +0100] rev 1672

Initial proof modifications for alpha_res

Sat, 27 Mar 2010 08:11:45 +0100 merge

changeset

Cezary Kaliszyk <kaliszyk@in.tum.de> [Sat, 27 Mar 2010 08:11:45 +0100] rev 1671

merge

Sat, 27 Mar 2010 08:11:11 +0100 Fv/Alpha now takes into account Alpha_Type given from the parser.

changeset

Cezary Kaliszyk <kaliszyk@in.tum.de> [Sat, 27 Mar 2010 08:11:11 +0100] rev 1670

Fv/Alpha now takes into account Alpha_Type given from the parser.

Sat, 27 Mar 2010 06:51:13 +0100 Minor cleaning.

changeset

Cezary Kaliszyk <kaliszyk@in.tum.de> [Sat, 27 Mar 2010 06:51:13 +0100] rev 1669

Minor cleaning.

Sat, 27 Mar 2010 06:44:47 +0100 merged

changeset

Christian Urban <urbanc@in.tum.de> [Sat, 27 Mar 2010 06:44:47 +0100] rev 1668

merged

Sat, 27 Mar 2010 06:44:14 +0100 more on the paper

changeset

Christian Urban <urbanc@in.tum.de> [Sat, 27 Mar 2010 06:44:14 +0100] rev 1667