2010-06-11 more intro
Christian Urban <urbanc@in.tum.de> [Fri, 11 Jun 2010 21:58:25 +0200] rev 2223
more intro
2010-06-11 more on the qpaper
Christian Urban <urbanc@in.tum.de> [Fri, 11 Jun 2010 17:52:06 +0200] rev 2222
more on the qpaper
2010-06-11 even more on the qpaper (intro almost done)
Christian Urban <urbanc@in.tum.de> [Fri, 11 Jun 2010 16:36:02 +0200] rev 2221
even more on the qpaper (intro almost done)
2010-06-11 more to the introduction of the qpaper
Christian Urban <urbanc@in.tum.de> [Fri, 11 Jun 2010 14:04:58 +0200] rev 2220
more to the introduction of the qpaper
2010-06-10 adapted to the official sigplan style file (this gives us more space)
Christian Urban <urbanc@in.tum.de> [Thu, 10 Jun 2010 13:37:32 +0200] rev 2219
adapted to the official sigplan style file (this gives us more space)
2010-06-10 added to the popl-paper a pointer to work by Altenkirch
Christian Urban <urbanc@in.tum.de> [Thu, 10 Jun 2010 13:28:38 +0200] rev 2218
added to the popl-paper a pointer to work by Altenkirch
2010-06-10 more on the qpaper
Christian Urban <urbanc@in.tum.de> [Thu, 10 Jun 2010 10:53:51 +0200] rev 2217
more on the qpaper
2010-06-07 new title for POPL paper
Christian Urban <urbanc@in.tum.de> [Mon, 07 Jun 2010 16:17:35 +0200] rev 2216
new title for POPL paper
2010-06-07 more work on intro and abstract (done for today)
Christian Urban <urbanc@in.tum.de> [Mon, 07 Jun 2010 15:57:03 +0200] rev 2215
more work on intro and abstract (done for today)
2010-06-07 a bit more in the introduction and abstract
Christian Urban <urbanc@in.tum.de> [Mon, 07 Jun 2010 15:13:39 +0200] rev 2214
a bit more in the introduction and abstract
2010-06-07 improved abstract, some tuning
Christian Urban <urbanc@in.tum.de> [Mon, 07 Jun 2010 11:33:00 +0200] rev 2213
improved abstract, some tuning
2010-06-06 Qpaper / minor on cleaning
Cezary Kaliszyk <kaliszyk@in.tum.de> [Sun, 06 Jun 2010 13:16:27 +0200] rev 2212
Qpaper / minor on cleaning
2010-06-05 qpaper / injection proof.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Sat, 05 Jun 2010 14:37:05 +0200] rev 2211
qpaper / injection proof.
2010-06-05 qpaper / example interaction
Cezary Kaliszyk <kaliszyk@in.tum.de> [Sat, 05 Jun 2010 10:03:42 +0200] rev 2210
qpaper / example interaction
2010-06-05 Qpaper/regularization proof.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Sat, 05 Jun 2010 08:02:39 +0200] rev 2209
Qpaper/regularization proof.
2010-06-05 qpaper
Cezary Kaliszyk <kaliszyk@in.tum.de> [Sat, 05 Jun 2010 07:26:22 +0200] rev 2208
qpaper
2010-06-02 Qpaper/more.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 02 Jun 2010 14:24:16 +0200] rev 2207
Qpaper/more.
2010-06-02 Qpaper/Minor
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 02 Jun 2010 13:58:37 +0200] rev 2206
Qpaper/Minor
2010-06-01 added larry's quote
Christian Urban <urbanc@in.tum.de> [Tue, 01 Jun 2010 15:58:59 +0200] rev 2205
added larry's quote
2010-06-01 added larry's paper
Christian Urban <urbanc@in.tum.de> [Tue, 01 Jun 2010 15:48:25 +0200] rev 2204
added larry's paper
2010-06-01 tuned
Christian Urban <urbanc@in.tum.de> [Tue, 01 Jun 2010 15:45:43 +0200] rev 2203
tuned
2010-05-28 first version of the abstract
Christian Urban <urbanc@in.tum.de> [Sat, 29 May 2010 00:16:39 +0200] rev 2202
first version of the abstract
2010-05-27 merged
Christian Urban <urbanc@in.tum.de> [Thu, 27 May 2010 18:30:42 +0200] rev 2201
merged
2010-05-27 fixed bug where perm_simp 'forgets' how to prove equivariance for the empty set
Christian Urban <urbanc@in.tum.de> [Thu, 27 May 2010 18:30:26 +0200] rev 2200
fixed bug where perm_simp 'forgets' how to prove equivariance for the empty set
2010-05-27 qpaper / lemmas used in proofs
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 27 May 2010 16:53:12 +0200] rev 2199
qpaper / lemmas used in proofs
2010-05-27 qpaper / injection statement
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 27 May 2010 16:33:10 +0200] rev 2198
qpaper / injection statement
2010-05-27 qpaper / regularize
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 27 May 2010 16:06:43 +0200] rev 2197
qpaper / regularize
2010-05-27 qpaper / a bit about prs
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 27 May 2010 14:30:07 +0200] rev 2196
qpaper / a bit about prs
2010-05-27 Functionalized the ABS/REP definition.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 27 May 2010 11:21:37 +0200] rev 2195
Functionalized the ABS/REP definition.
2010-05-26 qpaper / lifting introduction
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 26 May 2010 17:55:42 +0200] rev 2194
qpaper / lifting introduction
2010-05-26 merged
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 26 May 2010 17:20:59 +0200] rev 2193
merged
2010-05-26 fixed compile error
Christian Urban <urbanc@in.tum.de> [Wed, 26 May 2010 17:19:16 +0200] rev 2192
fixed compile error
2010-05-26 qpaper / composition of quotients.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 26 May 2010 17:10:05 +0200] rev 2191
qpaper / composition of quotients.
2010-05-26 qpaper
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 26 May 2010 16:56:38 +0200] rev 2190
qpaper
2010-05-26 qpaper..
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 26 May 2010 16:28:35 +0200] rev 2189
qpaper..
2010-05-26 qpaper.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 26 May 2010 16:17:49 +0200] rev 2188
qpaper.
2010-05-26 Name some respectfullness
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 26 May 2010 16:09:09 +0200] rev 2187
Name some respectfullness
2010-05-26 added FSet to the correct paper
Christian Urban <urbanc@in.tum.de> [Wed, 26 May 2010 15:35:34 +0200] rev 2186
added FSet to the correct paper
2010-05-26 merged
Christian Urban <urbanc@in.tum.de> [Wed, 26 May 2010 15:26:22 +0200] rev 2185
merged
2010-05-26 added FSet
Christian Urban <urbanc@in.tum.de> [Wed, 26 May 2010 15:26:00 +0200] rev 2184
added FSet
2010-05-26 qpaper
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 26 May 2010 15:24:33 +0200] rev 2183
qpaper
2010-05-26 qpaper
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 26 May 2010 12:11:58 +0200] rev 2182
qpaper
2010-05-25 Substitution Lemma for TypeSchemes.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 25 May 2010 18:38:52 +0200] rev 2181
Substitution Lemma for TypeSchemes.
2010-05-25 Simplified the proof
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 25 May 2010 17:29:05 +0200] rev 2180
Simplified the proof
2010-05-25 A lemma about substitution in TypeSchemes.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 25 May 2010 17:09:29 +0200] rev 2179
A lemma about substitution in TypeSchemes.
2010-05-25 reversing the direction of fresh_star
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 25 May 2010 17:01:37 +0200] rev 2178
reversing the direction of fresh_star
2010-05-25 overlapping deep binders proof
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 25 May 2010 10:43:19 +0200] rev 2177
overlapping deep binders proof
2010-05-25 edits from the reviewers
Christian Urban <urbanc@in.tum.de> [Tue, 25 May 2010 07:59:16 +0200] rev 2176
edits from the reviewers
2010-05-24 tuned paper
Christian Urban <urbanc@in.tum.de> [Mon, 24 May 2010 22:47:06 +0100] rev 2175
tuned paper
2010-05-23 changed qpaper to lncs-style
Christian Urban <urbanc@in.tum.de> [Sun, 23 May 2010 16:45:00 +0100] rev 2174
changed qpaper to lncs-style
2010-05-21 Match_Lam defined on Quotient Level.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 21 May 2010 17:17:51 +0200] rev 2173
Match_Lam defined on Quotient Level.
2010-05-21 More on Function-defined subst.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 21 May 2010 11:55:22 +0200] rev 2172
More on Function-defined subst.
2010-05-21 Isabelle renamings
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 21 May 2010 11:46:47 +0200] rev 2171
Isabelle renamings
2010-05-21 merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 21 May 2010 10:47:45 +0200] rev 2170
merge
2010-05-21 Renamings.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 21 May 2010 10:43:14 +0200] rev 2169
Renamings.
2010-05-21 Renamings
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 21 May 2010 10:42:53 +0200] rev 2168
Renamings
2010-05-21 merge (non-trival)
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 21 May 2010 10:47:07 +0200] rev 2167
merge (non-trival)
2010-05-21 Previously uncommited direct subst definition changes.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 21 May 2010 10:45:29 +0200] rev 2166
Previously uncommited direct subst definition changes.
2010-05-21 Function experiments
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 21 May 2010 10:44:07 +0200] rev 2165
Function experiments
2010-05-19 merged
Christian Urban <urbanc@in.tum.de> [Wed, 19 May 2010 12:44:03 +0100] rev 2164
merged
2010-05-19 added comments about pottiers work
Christian Urban <urbanc@in.tum.de> [Wed, 19 May 2010 12:43:38 +0100] rev 2163
added comments about pottiers work
2010-05-19 more subst experiments
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 19 May 2010 12:29:08 +0200] rev 2162
more subst experiments
2010-05-19 More subst experminets
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 19 May 2010 11:29:42 +0200] rev 2161
More subst experminets
2010-05-18 more on subst
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 18 May 2010 17:56:41 +0200] rev 2160
more on subst
2010-05-18 Single variable substitution
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 18 May 2010 17:17:54 +0200] rev 2159
Single variable substitution
2010-05-18 subst fix
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 18 May 2010 17:06:21 +0200] rev 2158
subst fix
2010-05-18 subst experiments
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 18 May 2010 15:58:52 +0200] rev 2157
subst experiments
2010-05-18 soem minor tuning
Christian Urban <urbanc@in.tum.de> [Tue, 18 May 2010 14:40:05 +0100] rev 2156
soem minor tuning
2010-05-18 Fix broken add
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 18 May 2010 11:47:29 +0200] rev 2155
Fix broken add
2010-05-18 add missing .bib
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 18 May 2010 11:46:58 +0200] rev 2154
add missing .bib
2010-05-18 merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 18 May 2010 11:46:19 +0200] rev 2153
merge
2010-05-18 starting bibliography
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 18 May 2010 11:45:49 +0200] rev 2152
starting bibliography
2010-05-17 merged
Christian Urban <urbanc@in.tum.de> [Mon, 17 May 2010 20:23:40 +0100] rev 2151
merged
2010-05-17 updated to new Isabelle (More_Conv -> Conv)
Christian Urban <urbanc@in.tum.de> [Mon, 17 May 2010 18:13:39 +0100] rev 2150
updated to new Isabelle (More_Conv -> Conv)
2010-05-17 made this example to work again
Christian Urban <urbanc@in.tum.de> [Mon, 17 May 2010 17:54:07 +0100] rev 2149
made this example to work again
2010-05-17 merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 17 May 2010 17:34:02 +0200] rev 2148
merge
2010-05-17 alpha_alphabn for bindings in a type under bn.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 17 May 2010 17:31:18 +0200] rev 2147
alpha_alphabn for bindings in a type under bn.
2010-05-17 minor tuning
Christian Urban <urbanc@in.tum.de> [Mon, 17 May 2010 16:25:45 +0100] rev 2146
minor tuning
2010-05-17 Ex4 does work, and I don't see the difference between the alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 17 May 2010 16:29:33 +0200] rev 2145
Ex4 does work, and I don't see the difference between the alphas.
2010-05-17 slight tuning
Christian Urban <urbanc@in.tum.de> [Mon, 17 May 2010 12:46:51 +0100] rev 2144
slight tuning
2010-05-17 somewhat simplified the main parsing function; failed to move a Note-statement to define_raw_perms
Christian Urban <urbanc@in.tum.de> [Mon, 17 May 2010 12:00:54 +0100] rev 2143
somewhat simplified the main parsing function; failed to move a Note-statement to define_raw_perms
2010-05-16 moved the exporting part into the parser (this is still a hack); re-added CoreHaskell again to the examples - there seems to be a problem with the variable name pat
Christian Urban <urbanc@in.tum.de> [Sun, 16 May 2010 12:41:27 +0100] rev 2142
moved the exporting part into the parser (this is still a hack); re-added CoreHaskell again to the examples - there seems to be a problem with the variable name pat
2010-05-16 tuned paper
Christian Urban <urbanc@in.tum.de> [Sun, 16 May 2010 11:00:44 +0100] rev 2141
tuned paper
2010-05-15 tuned paper
Christian Urban <urbanc@in.tum.de> [Sat, 15 May 2010 22:06:06 +0100] rev 2140
tuned paper
2010-05-14 tuned a bit the paper
Christian Urban <urbanc@in.tum.de> [Fri, 14 May 2010 21:18:34 +0100] rev 2139
tuned a bit the paper
2010-05-14 started a new file for the parser to make some experiments
Christian Urban <urbanc@in.tum.de> [Fri, 14 May 2010 18:12:07 +0100] rev 2138
started a new file for the parser to make some experiments
2010-05-14 moved old parser and fv into attic
Christian Urban <urbanc@in.tum.de> [Fri, 14 May 2010 17:58:26 +0100] rev 2137
moved old parser and fv into attic
2010-05-14 polished example
Christian Urban <urbanc@in.tum.de> [Fri, 14 May 2010 17:40:43 +0100] rev 2136
polished example
2010-05-14 merged
Christian Urban <urbanc@in.tum.de> [Fri, 14 May 2010 15:21:05 +0100] rev 2135
merged
2010-05-14 tuned a bit the paper
Christian Urban <urbanc@in.tum.de> [Fri, 14 May 2010 15:02:25 +0100] rev 2134
tuned a bit the paper
2010-05-14 Proper fv/alpha for multiple compound binders
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 14 May 2010 15:37:23 +0200] rev 2133
Proper fv/alpha for multiple compound binders
2010-05-14 SingleLetFoo with everything.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 14 May 2010 10:28:42 +0200] rev 2132
SingleLetFoo with everything.
2010-05-14 Fv for multiple binding functions
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 14 May 2010 10:21:14 +0200] rev 2131
Fv for multiple binding functions
2010-05-13 added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de> [Thu, 13 May 2010 19:06:54 +0100] rev 2130
added a more instructive example - has some problems with fv though
2010-05-13 added flip_eqvt and swap_eqvt to the equivariance lists
Christian Urban <urbanc@in.tum.de> [Thu, 13 May 2010 18:19:48 +0100] rev 2129
added flip_eqvt and swap_eqvt to the equivariance lists
2010-05-13 tuned the paper
Christian Urban <urbanc@in.tum.de> [Thu, 13 May 2010 17:41:28 +0100] rev 2128
tuned the paper
2010-05-13 properly declared outer keyword
Christian Urban <urbanc@in.tum.de> [Thu, 13 May 2010 16:09:34 +0100] rev 2127
properly declared outer keyword
2010-05-13 added an example which goes outside our current speciifcation
Christian Urban <urbanc@in.tum.de> [Thu, 13 May 2010 15:58:36 +0100] rev 2126
added an example which goes outside our current speciifcation
2010-05-13 made out of STEPS a configuration value so that it can be set individually in each file
Christian Urban <urbanc@in.tum.de> [Thu, 13 May 2010 15:58:02 +0100] rev 2125
made out of STEPS a configuration value so that it can be set individually in each file
2010-05-13 tuned eqvt-proofs about prod_rel and prod_fv
Christian Urban <urbanc@in.tum.de> [Thu, 13 May 2010 15:12:34 +0100] rev 2124
tuned eqvt-proofs about prod_rel and prod_fv
2010-05-13 removed internal functions from the signature (they are not needed anymore)
Christian Urban <urbanc@in.tum.de> [Thu, 13 May 2010 15:12:05 +0100] rev 2123
removed internal functions from the signature (they are not needed anymore)
2010-05-13 added term4 back to the examples
Christian Urban <urbanc@in.tum.de> [Thu, 13 May 2010 10:34:59 +0100] rev 2122
added term4 back to the examples
2010-05-13 Make Term4 use 'equivariance'.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 13 May 2010 07:41:18 +0200] rev 2121
Make Term4 use 'equivariance'.
2010-05-12 fixed the examples for the new eqvt-procedure....temporarily disabled Manual/Term4.thy
Christian Urban <urbanc@in.tum.de> [Wed, 12 May 2010 16:59:53 +0100] rev 2120
fixed the examples for the new eqvt-procedure....temporarily disabled Manual/Term4.thy
2010-05-12 merged
Christian Urban <urbanc@in.tum.de> [Wed, 12 May 2010 16:33:50 +0100] rev 2119
merged
2010-05-12 moved the data-transformation into the parser
Christian Urban <urbanc@in.tum.de> [Wed, 12 May 2010 16:33:25 +0100] rev 2118
moved the data-transformation into the parser
2010-05-12 added a test whether some of the constants already equivariant (then the procedure has to fail).
Christian Urban <urbanc@in.tum.de> [Wed, 12 May 2010 16:26:06 +0100] rev 2117
added a test whether some of the constants already equivariant (then the procedure has to fail).
2010-05-12 include set_simps and append_simps in fv_rsp
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 12 May 2010 16:57:01 +0200] rev 2116
include set_simps and append_simps in fv_rsp
2010-05-12 Move alpha_eqvt to unused.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 12 May 2010 16:39:10 +0200] rev 2115
Move alpha_eqvt to unused.
2010-05-12 Use equivariance instead of alpha_eqvt
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 12 May 2010 16:32:44 +0200] rev 2114
Use equivariance instead of alpha_eqvt
2010-05-12 merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 12 May 2010 16:18:04 +0200] rev 2113
merge
2010-05-12 merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 12 May 2010 16:11:23 +0200] rev 2112
merge
2010-05-12 fvbv_rsp include prod_rel.simps
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 12 May 2010 16:11:03 +0200] rev 2111
fvbv_rsp include prod_rel.simps
2010-05-12 better ML-interface (returning only a list of theorems and a context)
Christian Urban <urbanc@in.tum.de> [Wed, 12 May 2010 15:17:35 +0100] rev 2110
better ML-interface (returning only a list of theorems and a context)
2010-05-12 merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 12 May 2010 16:09:38 +0200] rev 2109
merge
2010-05-12 Use raw_induct instead of induct
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 12 May 2010 16:08:32 +0200] rev 2108
Use raw_induct instead of induct
2010-05-12 ingnored parameters in equivariance; added a proper interface to be called from ML
Christian Urban <urbanc@in.tum.de> [Wed, 12 May 2010 14:47:52 +0100] rev 2107
ingnored parameters in equivariance; added a proper interface to be called from ML
2010-05-12 properly exported defined bn-functions
Christian Urban <urbanc@in.tum.de> [Wed, 12 May 2010 13:43:48 +0100] rev 2106
properly exported defined bn-functions
2010-05-11 Include raw permutation definitions in eqvt
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 11 May 2010 18:20:25 +0200] rev 2105
Include raw permutation definitions in eqvt
2010-05-11 Declare alpha_gen_eqvt as eqvt and change the proofs that used 'eqvts[symmetric]'
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 11 May 2010 17:16:57 +0200] rev 2104
Declare alpha_gen_eqvt as eqvt and change the proofs that used 'eqvts[symmetric]'
2010-05-11 a bit for the introduction of the q-paper
Christian Urban <urbanc@in.tum.de> [Tue, 11 May 2010 14:58:46 +0100] rev 2103
a bit for the introduction of the q-paper
2010-05-11 added some of the quotient literature; a bit more to the qpaper
Christian Urban <urbanc@in.tum.de> [Tue, 11 May 2010 12:18:26 +0100] rev 2102
added some of the quotient literature; a bit more to the qpaper
2010-05-10 fixed a problem with non-existant alphas2
Christian Urban <urbanc@in.tum.de> [Mon, 10 May 2010 18:09:00 +0100] rev 2101
fixed a problem with non-existant alphas2
2010-05-10 added comment about bind_set
Christian Urban <urbanc@in.tum.de> [Mon, 10 May 2010 17:57:22 +0100] rev 2100
added comment about bind_set
2010-05-10 fixing bind_set problem
Christian Urban <urbanc@in.tum.de> [Mon, 10 May 2010 17:55:54 +0100] rev 2099
fixing bind_set problem
2010-05-10 merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 10 May 2010 18:32:50 +0200] rev 2098
merge
2010-05-10 Term8 comment
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 10 May 2010 18:32:15 +0200] rev 2097
Term8 comment
2010-05-10 merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 10 May 2010 18:30:27 +0200] rev 2096
merge
2010-05-10 Restore set bindings in CoreHaskell
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 10 May 2010 18:29:45 +0200] rev 2095
Restore set bindings in CoreHaskell
2010-05-10 Recursive examples with relation composition
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 10 May 2010 15:54:16 +0200] rev 2094
Recursive examples with relation composition
2010-05-10 merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 10 May 2010 15:45:04 +0200] rev 2093
merge
2010-05-10 prod_rel and prod_fv eqvt and mono
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 10 May 2010 15:44:49 +0200] rev 2092
prod_rel and prod_fv eqvt and mono
2010-05-10 ExLetRec
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 10 May 2010 15:14:02 +0200] rev 2091
ExLetRec
2010-05-10 merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 10 May 2010 15:11:19 +0200] rev 2090
merge
2010-05-10 Parser changes for compound relations
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 10 May 2010 15:11:05 +0200] rev 2089
Parser changes for compound relations
2010-05-10 merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 10 May 2010 15:09:53 +0200] rev 2088
merge
2010-05-10 Use mk_compound_fv' and mk_compound_rel'
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 10 May 2010 15:09:32 +0200] rev 2087
Use mk_compound_fv' and mk_compound_rel'
2010-05-10 merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 10 May 2010 12:05:13 +0200] rev 2086
merge
2010-05-10 Membership in a pair of lists.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 10 May 2010 12:04:40 +0200] rev 2085
Membership in a pair of lists.
2010-05-10 Synchronize FSet with repository
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 10 May 2010 10:22:57 +0200] rev 2084
Synchronize FSet with repository
2010-05-09 tuned file names for examples
Christian Urban <urbanc@in.tum.de> [Sun, 09 May 2010 12:38:59 +0100] rev 2083
tuned file names for examples
2010-05-09 cleaned up a bit the examples; added equivariance to all examples
Christian Urban <urbanc@in.tum.de> [Sun, 09 May 2010 12:26:10 +0100] rev 2082
cleaned up a bit the examples; added equivariance to all examples
2010-05-09 fixed the problem with alpha containing splits
Christian Urban <urbanc@in.tum.de> [Sun, 09 May 2010 11:43:24 +0100] rev 2081
fixed the problem with alpha containing splits
2010-05-09 added eqvt-lemma for split; changed semantics of perm_simp: excluded stands for constants about which no complaint is written out...eqvt_apply is now always applied
Christian Urban <urbanc@in.tum.de> [Sun, 09 May 2010 11:37:19 +0100] rev 2080
added eqvt-lemma for split; changed semantics of perm_simp: excluded stands for constants about which no complaint is written out...eqvt_apply is now always applied
2010-05-07 Manually added some newer keywords from the distribution
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 07 May 2010 12:28:11 +0200] rev 2079
Manually added some newer keywords from the distribution
2010-05-07 Regularize experiments
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 07 May 2010 12:10:04 +0200] rev 2078
Regularize experiments
2010-05-06 alpha_eqvt_tac with prod_rel and prod_fv simps
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 06 May 2010 14:21:10 +0200] rev 2077
alpha_eqvt_tac with prod_rel and prod_fv simps
2010-05-06 mem => member
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 06 May 2010 14:14:30 +0200] rev 2076
mem => member
2010-05-06 merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 06 May 2010 14:13:45 +0200] rev 2075
merge
2010-05-06 Fixes for new Isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 06 May 2010 14:13:35 +0200] rev 2074
Fixes for new Isabelle
2010-05-06 compound versions with prod_rel and prod_fun, not made default yet.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 06 May 2010 14:13:05 +0200] rev 2073
compound versions with prod_rel and prod_fun, not made default yet.
2010-05-06 prod_rel and prod_fv simps
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 06 May 2010 14:10:56 +0200] rev 2072
prod_rel and prod_fv simps
2010-05-06 mem => member
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 06 May 2010 14:10:26 +0200] rev 2071
mem => member
2010-05-06 prod_rel.simps and Fixed for new isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 06 May 2010 14:09:56 +0200] rev 2070
prod_rel.simps and Fixed for new isabelle
2010-05-06 Fixes for new isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 06 May 2010 14:09:21 +0200] rev 2069
Fixes for new isabelle
2010-05-06 prod_fv and its respectfullness and preservation.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 06 May 2010 13:25:37 +0200] rev 2068
prod_fv and its respectfullness and preservation.
2010-05-06 Experiments with equivariance.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 06 May 2010 10:43:41 +0200] rev 2067
Experiments with equivariance.
2010-05-05 merged
Christian Urban <urbanc@in.tum.de> [Wed, 05 May 2010 20:39:56 +0100] rev 2066
merged
2010-05-05 a bit mor on the pearl journal paper
Christian Urban <urbanc@in.tum.de> [Wed, 05 May 2010 20:39:21 +0100] rev 2065
a bit mor on the pearl journal paper
2010-05-05 solved the problem with equivariance by first eta-normalising the goal
Christian Urban <urbanc@in.tum.de> [Wed, 05 May 2010 10:24:54 +0100] rev 2064
solved the problem with equivariance by first eta-normalising the goal
2010-05-05 Some cleaning in Term4
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 05 May 2010 09:23:10 +0200] rev 2063
Some cleaning in Term4
2010-05-04 "isabelle make" compiles all examples with newparser/newfv/newalpha only.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 04 May 2010 17:25:58 +0200] rev 2062
"isabelle make" compiles all examples with newparser/newfv/newalpha only.
2010-05-04 Move Term4 to NewParser
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 04 May 2010 17:15:21 +0200] rev 2061
Move Term4 to NewParser
2010-05-04 Fix Term4 for permutation signature change
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 04 May 2010 16:59:31 +0200] rev 2060
Fix Term4 for permutation signature change
2010-05-04 Move LF to NewParser. Just works.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 04 May 2010 16:44:12 +0200] rev 2059
Move LF to NewParser. Just works.
2010-05-04 merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 04 May 2010 16:42:36 +0200] rev 2058
merge
2010-05-04 ExLetMult
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 04 May 2010 16:42:28 +0200] rev 2057
ExLetMult
2010-05-04 Ex1Rec.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 04 May 2010 16:39:12 +0200] rev 2056
Ex1Rec.
2010-05-04 merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 04 May 2010 16:33:38 +0200] rev 2055
merge
2010-05-04 merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 04 May 2010 16:33:30 +0200] rev 2054
merge
2010-05-04 ExPS3 in NewParser
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 04 May 2010 16:29:11 +0200] rev 2053
ExPS3 in NewParser
2010-05-04 Move ExPS8 to new parser.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 04 May 2010 16:22:21 +0200] rev 2052
Move ExPS8 to new parser.
2010-05-04 Fix for new isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 04 May 2010 16:30:31 +0200] rev 2051
Fix for new isabelle
2010-05-04 merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 04 May 2010 16:18:07 +0200] rev 2050
merge
2010-05-04 Minor
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 04 May 2010 16:17:46 +0200] rev 2049
Minor
2010-05-04 increased step counter so that all steps go through
Christian Urban <urbanc@in.tum.de> [Tue, 04 May 2010 14:38:07 +0100] rev 2048
increased step counter so that all steps go through
2010-05-04 fixed my error with define_raw_fv
Christian Urban <urbanc@in.tum.de> [Tue, 04 May 2010 14:33:50 +0100] rev 2047
fixed my error with define_raw_fv
2010-05-04 tuned and added some comments to the code; added also an exception for early exit of the nominal2_cmd function
Christian Urban <urbanc@in.tum.de> [Tue, 04 May 2010 14:25:22 +0100] rev 2046
tuned and added some comments to the code; added also an exception for early exit of the nominal2_cmd function
2010-05-04 Separate Term8, as it may work soon.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 04 May 2010 14:21:18 +0200] rev 2045
Separate Term8, as it may work soon.
2010-05-04 moved CoreHaskell to NewParser.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 04 May 2010 14:13:18 +0200] rev 2044
moved CoreHaskell to NewParser.
2010-05-04 ExPS7 in NewParser
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 04 May 2010 13:52:40 +0200] rev 2043
ExPS7 in NewParser
2010-05-04 Move ExLeroy to New Parser
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 04 May 2010 12:34:33 +0200] rev 2042
Move ExLeroy to New Parser
2010-05-04 Move 2 more to NewParser
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 04 May 2010 11:22:22 +0200] rev 2041
Move 2 more to NewParser
2010-05-04 Move TypeSchemes to NewParser
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 04 May 2010 11:12:09 +0200] rev 2040
Move TypeSchemes to NewParser
2010-05-04 Move ExLet to NewParser.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 04 May 2010 11:08:30 +0200] rev 2039
Move ExLet to NewParser.
2010-05-04 tuned
Christian Urban <urbanc@in.tum.de> [Tue, 04 May 2010 07:22:33 +0100] rev 2038
tuned
2010-05-04 roll back of the last commit (there was a difference)
Christian Urban <urbanc@in.tum.de> [Tue, 04 May 2010 06:24:54 +0100] rev 2037
roll back of the last commit (there was a difference)
2010-05-04 tuned
Christian Urban <urbanc@in.tum.de> [Tue, 04 May 2010 06:05:13 +0100] rev 2036
tuned
2010-05-04 to my best knowledge the number of datatypes is equal to the length of the dt_descr; so we can save one argument in define_raw_perm
Christian Urban <urbanc@in.tum.de> [Tue, 04 May 2010 06:02:45 +0100] rev 2035
to my best knowledge the number of datatypes is equal to the length of the dt_descr; so we can save one argument in define_raw_perm
2010-05-04 merged
Christian Urban <urbanc@in.tum.de> [Tue, 04 May 2010 05:36:55 +0100] rev 2034
merged
2010-05-04 some preliminary changes to the pearl-jv paper
Christian Urban <urbanc@in.tum.de> [Tue, 04 May 2010 05:36:43 +0100] rev 2033
some preliminary changes to the pearl-jv paper
2010-05-03 some preliminary notes of the abstract (qpaper); still need to see the motivating example
Christian Urban <urbanc@in.tum.de> [Mon, 03 May 2010 08:52:15 +0100] rev 2032
some preliminary notes of the abstract (qpaper); still need to see the motivating example
2010-05-03 Added cheats to classical
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 03 May 2010 15:47:30 +0200] rev 2031
Added cheats to classical
2010-05-03 Ex2 moved to new parser.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 03 May 2010 15:38:20 +0200] rev 2030
Ex2 moved to new parser.
2010-05-03 alpha_eqvt_tac fixed to work when the existential is not at the top level.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 03 May 2010 15:37:21 +0200] rev 2029
alpha_eqvt_tac fixed to work when the existential is not at the top level.
2010-05-03 SingleLet and Ex3 work with NewParser.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 03 May 2010 15:36:47 +0200] rev 2028
SingleLet and Ex3 work with NewParser.
2010-05-03 Comment
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 03 May 2010 15:13:15 +0200] rev 2027
Comment
2010-05-03 Another example where only alpha_eqvt fails.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 03 May 2010 14:31:11 +0200] rev 2026
Another example where only alpha_eqvt fails.
2010-05-03 Register only non-looping rules in eq_iff
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 03 May 2010 14:30:37 +0200] rev 2025
Register only non-looping rules in eq_iff
2010-05-03 Equivariance fails for single let?
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 03 May 2010 14:03:30 +0200] rev 2024
Equivariance fails for single let?
2010-05-03 NewParser
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 03 May 2010 13:42:44 +0200] rev 2023
NewParser
2010-05-03 Introduce eq_iff_simp to match the one from Parser.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 03 May 2010 12:24:27 +0200] rev 2022
Introduce eq_iff_simp to match the one from Parser.
2010-05-03 remove tracing
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 03 May 2010 11:43:27 +0200] rev 2021
remove tracing
2010-05-03 Cheat support equations in new parser
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 03 May 2010 11:43:08 +0200] rev 2020
Cheat support equations in new parser
2010-05-03 Remove dependency on NewFv
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 03 May 2010 11:37:44 +0200] rev 2019
Remove dependency on NewFv
2010-05-03 Fix Parser
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 03 May 2010 11:35:38 +0200] rev 2018
Fix Parser
2010-05-03 Add explicit cheats in NewParser and comment out the examples for outside use.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 03 May 2010 10:15:23 +0200] rev 2017
Add explicit cheats in NewParser and comment out the examples for outside use.
2010-05-03 Fix Datatype_Aux calls in NewParser.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 03 May 2010 09:57:05 +0200] rev 2016
Fix Datatype_Aux calls in NewParser.
2010-05-03 Move old fv_alpha_export to Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 03 May 2010 09:55:43 +0200] rev 2015
Move old fv_alpha_export to Fv.
2010-05-02 moved old parser and old fv back into their original places; isabelle make works again
Christian Urban <urbanc@in.tum.de> [Mon, 03 May 2010 00:01:12 +0100] rev 2014
moved old parser and old fv back into their original places; isabelle make works again
2010-05-02 slight tuning
Christian Urban <urbanc@in.tum.de> [Mon, 03 May 2010 00:00:33 +0100] rev 2013
slight tuning
2010-05-02 simplified the supp-of-finite-sets proof
Christian Urban <urbanc@in.tum.de> [Sun, 02 May 2010 21:15:52 +0100] rev 2012
simplified the supp-of-finite-sets proof
2010-05-02 tried to add some comments in the huge(!) nominal2_cmd function
Christian Urban <urbanc@in.tum.de> [Sun, 02 May 2010 16:02:27 +0100] rev 2011
tried to add some comments in the huge(!) nominal2_cmd function
2010-05-02 replaced make_pair with library function HOLogic.mk_prod
Christian Urban <urbanc@in.tum.de> [Sun, 02 May 2010 16:01:45 +0100] rev 2010
replaced make_pair with library function HOLogic.mk_prod
2010-05-02 removed duplicate eqvt attribute
Christian Urban <urbanc@in.tum.de> [Sun, 02 May 2010 16:00:52 +0100] rev 2009
removed duplicate eqvt attribute
2010-05-02 attempted to remove dependency on (old) Fv and (old) Parser; lifting still uses Fv.thy; the examples do not work at the moment (with equivp proofs failing)
Christian Urban <urbanc@in.tum.de> [Sun, 02 May 2010 14:06:26 +0100] rev 2008
attempted to remove dependency on (old) Fv and (old) Parser; lifting still uses Fv.thy; the examples do not work at the moment (with equivp proofs failing)
2010-05-01 merged
Christian Urban <urbanc@in.tum.de> [Sat, 01 May 2010 09:15:46 +0100] rev 2007
merged
2010-05-01 tuned
Christian Urban <urbanc@in.tum.de> [Sat, 01 May 2010 09:14:25 +0100] rev 2006
tuned
2010-04-30 replaced hide by the new hide_const
Christian Urban <urbanc@in.tum.de> [Fri, 30 Apr 2010 16:31:43 +0100] rev 2005
replaced hide by the new hide_const
2010-04-30 generalised the fs-instance lemma (not just fsets of atoms are finitely supported, but also fsets of finitely supported elements)
Christian Urban <urbanc@in.tum.de> [Fri, 30 Apr 2010 15:36:02 +0100] rev 2004
generalised the fs-instance lemma (not just fsets of atoms are finitely supported, but also fsets of finitely supported elements)
2010-04-30 added lemmas establishing the support of finite sets of finitely supported elements
Christian Urban <urbanc@in.tum.de> [Fri, 30 Apr 2010 15:34:26 +0100] rev 2003
added lemmas establishing the support of finite sets of finitely supported elements
2010-04-30 added eqvt-lemmas for Bex, Ball and Union
Christian Urban <urbanc@in.tum.de> [Fri, 30 Apr 2010 14:21:18 +0100] rev 2002
added eqvt-lemmas for Bex, Ball and Union
2010-04-30 NewParser with Parser functionality, but some cheats included since the order of datayupes is wrong.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 30 Apr 2010 15:45:39 +0200] rev 2001
NewParser with Parser functionality, but some cheats included since the order of datayupes is wrong.
2010-04-30 Merged nominal_datatype into NewParser until eqvts
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 30 Apr 2010 14:48:13 +0200] rev 2000
Merged nominal_datatype into NewParser until eqvts
2010-04-30 more parser/new parser synchronization.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 30 Apr 2010 13:57:59 +0200] rev 1999
more parser/new parser synchronization.
2010-04-30 Simplify old parser for integration
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 30 Apr 2010 10:48:48 +0200] rev 1998
Simplify old parser for integration
2010-04-30 merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 30 Apr 2010 10:32:34 +0200] rev 1997
merge
2010-04-30 Change signature of fv and alpha generation.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 30 Apr 2010 10:31:32 +0200] rev 1996
Change signature of fv and alpha generation.
2010-04-30 reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de> [Fri, 30 Apr 2010 10:09:45 +0100] rev 1995
reorganised eqvt-file (now uses perm_simp already)
2010-04-30 qpaper
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 30 Apr 2010 10:04:24 +0200] rev 1994
qpaper
2010-04-29 merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 29 Apr 2010 17:52:33 +0200] rev 1993
merge
2010-04-29 New Alpha.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 29 Apr 2010 17:52:19 +0200] rev 1992
New Alpha.
2010-04-29 Minimal cleaning in LamEx
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 29 Apr 2010 17:16:35 +0200] rev 1991
Minimal cleaning in LamEx
2010-04-29 Remove things moved to the isabelle distribution
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 29 Apr 2010 17:03:59 +0200] rev 1990
Remove things moved to the isabelle distribution
2010-04-29 Unify and give only one name to 'setify', 'listify' and 'set'
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 29 Apr 2010 16:59:33 +0200] rev 1989
Unify and give only one name to 'setify', 'listify' and 'set'
2010-04-29 Fixing the definitions in the Parser.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 29 Apr 2010 16:18:38 +0200] rev 1988
Fixing the definitions in the Parser.
2010-04-29 Some of the exceptions that the parser should check in TODO.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 29 Apr 2010 16:16:45 +0200] rev 1987
Some of the exceptions that the parser should check in TODO.
2010-04-29 Extracting the fv body function and exporting the terms.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 29 Apr 2010 16:15:49 +0200] rev 1986
Extracting the fv body function and exporting the terms.
2010-04-29 Fix for recursive binders.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 29 Apr 2010 13:19:12 +0200] rev 1985
Fix for recursive binders.
2010-04-29 revert 0c9ef14e9ba4
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 29 Apr 2010 12:11:44 +0200] rev 1984
revert 0c9ef14e9ba4
(0) -1000 -240 +240 +1000 tip