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.
Mon, 19 Apr 2010 11:55:12 +0200 Getting rid of 'metis'.
changeset
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 19 Apr 2010 11:55:12 +0200] rev 1883
Getting rid of 'metis'.
Mon, 19 Apr 2010 11:38:43 +0200 merge
changeset
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 19 Apr 2010 11:38:43 +0200] rev 1882
merge
Mon, 19 Apr 2010 11:32:33 +0200 Remove 'defer'.
changeset
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 19 Apr 2010 11:32:33 +0200] rev 1881
Remove 'defer'.
Mon, 19 Apr 2010 09:27:53 +0200 merged
changeset
Christian Urban <urbanc@in.tum.de> [Mon, 19 Apr 2010 09:27:53 +0200] rev 1880
merged
Mon, 19 Apr 2010 09:25:31 +0200 tuned proofs
changeset
Christian Urban <urbanc@in.tum.de> [Mon, 19 Apr 2010 09:25:31 +0200] rev 1879
tuned proofs
Mon, 19 Apr 2010 11:04:31 +0200 2 more lifted lemmas needed for second representation
changeset
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 19 Apr 2010 11:04:31 +0200] rev 1878
2 more lifted lemmas needed for second representation
Mon, 19 Apr 2010 10:35:08 +0200 Accept non-equality eqvt rules in support proofs.
changeset
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 19 Apr 2010 10:35:08 +0200] rev 1877
Accept non-equality eqvt rules in support proofs.
Mon, 19 Apr 2010 10:00:52 +0200 merge
changeset
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 19 Apr 2010 10:00:52 +0200] rev 1876
merge
Mon, 19 Apr 2010 09:59:32 +0200 Locations of files in Parser
changeset
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 19 Apr 2010 09:59:32 +0200] rev 1875
Locations of files in Parser
Mon, 19 Apr 2010 09:25:55 +0200 merge
changeset
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 19 Apr 2010 09:25:55 +0200] rev 1874
merge
Mon, 19 Apr 2010 09:25:43 +0200 minor FSet3 edits.
changeset
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 19 Apr 2010 09:25:43 +0200] rev 1873
minor FSet3 edits.
Sun, 18 Apr 2010 18:01:22 +0200 tuned
changeset
Christian Urban <urbanc@in.tum.de> [Sun, 18 Apr 2010 18:01:22 +0200] rev 1872
tuned
Sun, 18 Apr 2010 17:58:45 +0200 moved some general function into nominal_library.ML
changeset
Christian Urban <urbanc@in.tum.de> [Sun, 18 Apr 2010 17:58:45 +0200] rev 1871
moved some general function into nominal_library.ML
Sun, 18 Apr 2010 17:57:27 +0200 tuned; transformation functions now take a context, a thm and return a thm
changeset
Christian Urban <urbanc@in.tum.de> [Sun, 18 Apr 2010 17:57:27 +0200] rev 1870
tuned; transformation functions now take a context, a thm and return a thm
Sun, 18 Apr 2010 17:56:05 +0200 tuned
changeset
Christian Urban <urbanc@in.tum.de> [Sun, 18 Apr 2010 17:56:05 +0200] rev 1869
tuned
Sun, 18 Apr 2010 10:58:29 +0200 equivariance for alpha_raw in CoreHaskell is automatically derived
changeset
Christian Urban <urbanc@in.tum.de> [Sun, 18 Apr 2010 10:58:29 +0200] rev 1868
equivariance for alpha_raw in CoreHaskell is automatically derived
Sun, 18 Apr 2010 09:26:38 +0200 preliminary parser for perm_simp metod
changeset
Christian Urban <urbanc@in.tum.de> [Sun, 18 Apr 2010 09:26:38 +0200] rev 1867
preliminary parser for perm_simp metod
Fri, 16 Apr 2010 16:29:11 +0200 automatic proofs for equivariance of alphas
changeset
Christian Urban <urbanc@in.tum.de> [Fri, 16 Apr 2010 16:29:11 +0200] rev 1866
automatic proofs for equivariance of alphas
Fri, 16 Apr 2010 11:09:32 +0200 Finished proof in Lambda.thy
changeset
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 16 Apr 2010 11:09:32 +0200] rev 1865
Finished proof in Lambda.thy
Fri, 16 Apr 2010 10:47:13 +0200 merged
changeset
Christian Urban <urbanc@in.tum.de> [Fri, 16 Apr 2010 10:47:13 +0200] rev 1864
merged
Fri, 16 Apr 2010 10:46:50 +0200 attempt to manual prove eqvt for alpha
changeset
Christian Urban <urbanc@in.tum.de> [Fri, 16 Apr 2010 10:46:50 +0200] rev 1863
attempt to manual prove eqvt for alpha
Fri, 16 Apr 2010 10:41:40 +0200 Lifting in Term4.
changeset
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 16 Apr 2010 10:41:40 +0200] rev 1862
Lifting in Term4.
Fri, 16 Apr 2010 10:18:16 +0200 some tuning of eqvt-infrastructure
changeset
Christian Urban <urbanc@in.tum.de> [Fri, 16 Apr 2010 10:18:16 +0200] rev 1861
some tuning of eqvt-infrastructure
Thu, 15 Apr 2010 21:56:03 +0200 some tuning of proofs
changeset
Christian Urban <urbanc@in.tum.de> [Thu, 15 Apr 2010 21:56:03 +0200] rev 1860
some tuning of proofs
Thu, 15 Apr 2010 16:01:28 +0200 typo
changeset
Christian Urban <urbanc@in.tum.de> [Thu, 15 Apr 2010 16:01:28 +0200] rev 1859
typo
Thu, 15 Apr 2010 15:56:38 +0200 merged
changeset
Christian Urban <urbanc@in.tum.de> [Thu, 15 Apr 2010 15:56:38 +0200] rev 1858
merged
Thu, 15 Apr 2010 15:56:21 +0200 half of the pair-abs-equivalence
changeset
Christian Urban <urbanc@in.tum.de> [Thu, 15 Apr 2010 15:56:21 +0200] rev 1857
half of the pair-abs-equivalence
Thu, 15 Apr 2010 15:31:36 +0200 More on Manual/Trm4
changeset
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 15 Apr 2010 15:31:36 +0200] rev 1856
More on Manual/Trm4
Thu, 15 Apr 2010 14:08:08 +0200 alpha4_equivp and constant lifting.
changeset
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 15 Apr 2010 14:08:08 +0200] rev 1855
alpha4_equivp and constant lifting.
Thu, 15 Apr 2010 13:55:44 +0200 alpha4_eqvt and alpha4_reflp
changeset
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 15 Apr 2010 13:55:44 +0200] rev 1854
alpha4_eqvt and alpha4_reflp
Thu, 15 Apr 2010 12:27:36 +0200 fv_eqvt in term4
changeset
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 15 Apr 2010 12:27:36 +0200] rev 1853
fv_eqvt in term4
Thu, 15 Apr 2010 12:15:38 +0200 Updating in Term4.
changeset
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 15 Apr 2010 12:15:38 +0200] rev 1852
Updating in Term4.
Thu, 15 Apr 2010 12:08:46 +0200 merge
changeset
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 15 Apr 2010 12:08:46 +0200] rev 1851
merge
Thu, 15 Apr 2010 11:42:28 +0200 Prove insert_rsp2
changeset
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 15 Apr 2010 11:42:28 +0200] rev 1850
Prove insert_rsp2
Thu, 15 Apr 2010 12:07:54 +0200 merged
changeset
Christian Urban <urbanc@in.tum.de> [Thu, 15 Apr 2010 12:07:54 +0200] rev 1849
merged
Thu, 15 Apr 2010 12:07:34 +0200 changed header
changeset
Christian Urban <urbanc@in.tum.de> [Thu, 15 Apr 2010 12:07:34 +0200] rev 1848
changed header
Thu, 15 Apr 2010 11:05:54 +0200 Minor paper fixes.
changeset
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 15 Apr 2010 11:05:54 +0200] rev 1847
Minor paper fixes.
Wed, 14 Apr 2010 22:41:22 +0200 temporary fix for CoreHaskell
changeset
Christian Urban <urbanc@in.tum.de> [Wed, 14 Apr 2010 22:41:22 +0200] rev 1846
temporary fix for CoreHaskell
Wed, 14 Apr 2010 22:23:52 +0200 deleted offending [eqvt]-attribute in Abs; Lambda works again, but there is now a problem in CoreHaskell
changeset
Christian Urban <urbanc@in.tum.de> [Wed, 14 Apr 2010 22:23:52 +0200] rev 1845
deleted offending [eqvt]-attribute in Abs; Lambda works again, but there is now a problem in CoreHaskell
Wed, 14 Apr 2010 20:21:11 +0200 merge
changeset
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 14 Apr 2010 20:21:11 +0200] rev 1844
merge
Wed, 14 Apr 2010 20:20:54 +0200 Fix the 'subscript' error.
changeset
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 14 Apr 2010 20:20:54 +0200] rev 1843
Fix the 'subscript' error.
Wed, 14 Apr 2010 18:47:20 +0200 merged
changeset
Christian Urban <urbanc@in.tum.de> [Wed, 14 Apr 2010 18:47:20 +0200] rev 1842
merged
Wed, 14 Apr 2010 18:46:59 +0200 thmdecls can deal with lemmas like alpha_gen which contain pairs or tuples
changeset
Christian Urban <urbanc@in.tum.de> [Wed, 14 Apr 2010 18:46:59 +0200] rev 1841
thmdecls can deal with lemmas like alpha_gen which contain pairs or tuples
Wed, 14 Apr 2010 16:11:04 +0200 merge
changeset
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 14 Apr 2010 16:11:04 +0200] rev 1840
merge
Wed, 14 Apr 2010 16:10:44 +0200 merge
changeset
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 14 Apr 2010 16:10:44 +0200] rev 1839
merge
Wed, 14 Apr 2010 11:08:33 +0200 Separate alpha_definition.
changeset
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 14 Apr 2010 11:08:33 +0200] rev 1838
Separate alpha_definition.
Wed, 14 Apr 2010 11:07:42 +0200 Fix spelling in theory header
changeset
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 14 Apr 2010 11:07:42 +0200] rev 1837
Fix spelling in theory header
Wed, 14 Apr 2010 10:50:11 +0200 Separate define_fv.
changeset
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 14 Apr 2010 10:50:11 +0200] rev 1836
Separate define_fv.
Wed, 14 Apr 2010 16:05:58 +0200 tuned and removed dead code
changeset
Christian Urban <urbanc@in.tum.de> [Wed, 14 Apr 2010 16:05:58 +0200] rev 1835
tuned and removed dead code
Wed, 14 Apr 2010 15:02:07 +0200 moved a couple of more functions to the library
changeset
Christian Urban <urbanc@in.tum.de> [Wed, 14 Apr 2010 15:02:07 +0200] rev 1834
moved a couple of more functions to the library
Wed, 14 Apr 2010 14:41:54 +0200 added a library for basic nominal functions; separated nominal_eqvt file
changeset
Christian Urban <urbanc@in.tum.de> [Wed, 14 Apr 2010 14:41:54 +0200] rev 1833
added a library for basic nominal functions; separated nominal_eqvt file
Wed, 14 Apr 2010 13:21:38 +0200 merged
changeset
Christian Urban <urbanc@in.tum.de> [Wed, 14 Apr 2010 13:21:38 +0200] rev 1832
merged
Wed, 14 Apr 2010 13:21:11 +0200 first working version of the automatic equivariance procedure
changeset
Christian Urban <urbanc@in.tum.de> [Wed, 14 Apr 2010 13:21:11 +0200] rev 1831
first working version of the automatic equivariance procedure
Wed, 14 Apr 2010 10:39:03 +0200 Initial cleaning/reorganization in Fv.
changeset
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 14 Apr 2010 10:39:03 +0200] rev 1830
Initial cleaning/reorganization in Fv.
Wed, 14 Apr 2010 10:29:56 +0200 merged
changeset
Christian Urban <urbanc@in.tum.de> [Wed, 14 Apr 2010 10:29:56 +0200] rev 1829
merged
Wed, 14 Apr 2010 10:29:34 +0200 preliminary tests
changeset
Christian Urban <urbanc@in.tum.de> [Wed, 14 Apr 2010 10:29:34 +0200] rev 1828
preliminary tests
Wed, 14 Apr 2010 10:28:17 +0200 deleted test
changeset
Christian Urban <urbanc@in.tum.de> [Wed, 14 Apr 2010 10:28:17 +0200] rev 1827
deleted test
Wed, 14 Apr 2010 08:42:38 +0200 merge
changeset
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 14 Apr 2010 08:42:38 +0200] rev 1826
merge
Wed, 14 Apr 2010 08:36:54 +0200 merge part: delete_rsp
changeset
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 14 Apr 2010 08:36:54 +0200] rev 1825
merge part: delete_rsp
Wed, 14 Apr 2010 08:35:31 +0200 merge part1: none_memb_nil
changeset
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 14 Apr 2010 08:35:31 +0200] rev 1824
merge part1: none_memb_nil
(0) -1000 -300 -100 -60 +60 +100 +300 +1000 tip
nominal2