# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1306893699 -32400
# Node ID 58eaa7fbf0e89036c577a083651e42e8f846a43a
# Parent  6750964a69bf7aba65e19149346970e4efa88de0
fixed previous commit

diff -r 6750964a69bf -r 58eaa7fbf0e8 Nominal/Ex/Lambda.thy
--- a/Nominal/Ex/Lambda.thy	Wed Jun 01 10:59:07 2011 +0900
+++ b/Nominal/Ex/Lambda.thy	Wed Jun 01 11:01:39 2011 +0900
@@ -383,7 +383,7 @@
   "dblam_in None = None"
 | "dblam_in (Some x) = Some (DBLam x)"
 
-lemma [eqvt]:
+lemma db_in_eqvt[eqvt]:
   "p \<bullet> (dbapp_in x y) = dbapp_in (p \<bullet> x) (p \<bullet> y)"
   "p \<bullet> (dblam_in x) = dblam_in (p \<bullet> x)"
   apply (case_tac [!] x)