Christian Urban <urbanc@in.tum.de> [Tue, 07 Aug 2012 18:53:50 +0100] rev 3196
tuned
Christian Urban <urbanc@in.tum.de> [Tue, 07 Aug 2012 16:55:17 +0100] rev 3195
added eqvt-lemma for function composition
Christian Urban <urbanc@in.tum.de> [Mon, 06 Aug 2012 13:50:19 +0100] rev 3194
added new ROOT session file
webertj [Fri, 03 Aug 2012 14:46:25 +0200] rev 3193
command_spec antiquotation.
Christian Urban <urbanc@in.tum.de> [Sun, 15 Jul 2012 13:03:47 +0100] rev 3192
added a simproc for alpha-equivalence to the simplifier
Christian Urban <urbanc@in.tum.de> [Thu, 12 Jul 2012 10:11:32 +0100] rev 3191
streamlined definition of alpha-equivalence for single binders (used flip instead of swap)
Christian Urban <urbanc@in.tum.de> [Mon, 18 Jun 2012 14:50:02 +0100] rev 3190
used ML-antiquotation command_spec for new commands
Christian Urban <urbanc@in.tum.de> [Tue, 12 Jun 2012 14:22:58 +0100] rev 3189
added eqvt for finfun_apply
Christian Urban <urbanc@in.tum.de> [Tue, 12 Jun 2012 13:56:16 +0100] rev 3188
improved the finfun parts
Christian Urban <urbanc@in.tum.de> [Tue, 12 Jun 2012 01:23:52 +0100] rev 3187
added finfun-type to Nominal
Christian Urban <urbanc@in.tum.de> [Mon, 11 Jun 2012 14:02:57 +0100] rev 3186
added CPS files to test (not all proofs have been completed)
Christian Urban <urbanc@in.tum.de> [Sat, 09 Jun 2012 19:48:19 +0100] rev 3185
added a rule about inequality of freshness between atoms to the simplifier
Christian Urban <urbanc@in.tum.de> [Wed, 06 Jun 2012 14:50:47 +0100] rev 3184
a simproc for simplifying Fresh when there is a sufficiently fresh atom
Christian Urban <urbanc@in.tum.de> [Mon, 04 Jun 2012 21:39:51 +0100] rev 3183
added permutation simplification to the simplifier; this makes the simplifier more powerful, but it potentially loops more often
Christian Urban <urbanc@in.tum.de> [Thu, 31 May 2012 12:01:13 +0100] rev 3182
merged
Christian Urban <urbanc@in.tum.de> [Thu, 31 May 2012 12:01:01 +0100] rev 3181
added to the simplifier nominal_datatype.fresh lemmas
Christian Urban <urbanc@in.tum.de> [Thu, 31 May 2012 11:59:56 +0100] rev 3180
added let-eqvt back
Cezary Kaliszyk <cezarykaliszyk@gmail.com> [Thu, 31 May 2012 12:44:37 +0200] rev 3179
Propagare changes from Nominal2_Base to _Exec
Christian Urban <urbanc@in.tum.de> [Thu, 31 May 2012 10:05:19 +0100] rev 3178
renamed fresh_fun to Fresh; added a simproc that deals with freshness of functions
Christian Urban <urbanc@in.tum.de> [Mon, 28 May 2012 18:03:06 +0100] rev 3177
added library routines for the constant fresh
Christian Urban <urbanc@in.tum.de> [Fri, 25 May 2012 15:46:48 +0100] rev 3176
fixed bug in simproc (also in the exec-version)
Cezary Kaliszyk <cezarykaliszyk@gmail.com> [Thu, 24 May 2012 10:17:32 +0200] rev 3175
Synchronize Nominal2_Base_Exec with Nominal2_Base, equivariance for Let, avoid overloading approx twice and changes for new isabelle
Christian Urban <urbanc@in.tum.de> [Wed, 23 May 2012 23:57:27 +0100] rev 3174
improved handling in the simplifier for inequalities derived from freshness assumptions
Cezary Kaliszyk <cezarykaliszyk@gmail.com> [Tue, 22 May 2012 14:55:58 +0200] rev 3173
Executing Lambda Terms
Cezary Kaliszyk <cezarykaliszyk@gmail.com> [Tue, 22 May 2012 14:00:59 +0200] rev 3172
Added workaround for broken quotient_type in tip isabelle.
Christian Urban <urbanc@in.tum.de> [Sat, 12 May 2012 22:24:04 +0100] rev 3171
further cleaning
Christian Urban <urbanc@in.tum.de> [Sat, 12 May 2012 22:21:25 +0100] rev 3170
cleaned also examples
Christian Urban <urbanc@in.tum.de> [Sat, 12 May 2012 21:39:09 +0100] rev 3169
cleaned the repository for Nominal2-Isabelle2012
Christian Urban <urbanc@in.tum.de> [Sat, 12 May 2012 21:05:59 +0100] rev 3168
Created branch for Isabelle-2012
Christian Urban <urbanc@in.tum.de> [Sat, 12 May 2012 20:54:00 +0100] rev 3167
added a lemma about composition and permutations