# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1274882949 -7200
# Node ID f9cc69b432ffadee554a8b49c186158606b8e253
# Parent  762a739c9eb477980a079c6d86cc05f7ad517f7e
Name some respectfullness

diff -r 762a739c9eb4 -r f9cc69b432ff Nominal/FSet.thy
--- a/Nominal/FSet.thy	Wed May 26 15:35:34 2010 +0200
+++ b/Nominal/FSet.thy	Wed May 26 16:09:09 2010 +0200
@@ -160,7 +160,7 @@
 
 text {* Respectfullness *}
 
-lemma [quot_respect]:
+lemma append_rsp[quot_respect]:
   shows "(op \<approx> ===> op \<approx> ===> op \<approx>) op @ op @"
   by auto
 
@@ -350,7 +350,7 @@
   then show ?thesis using f i by auto
 qed
 
-lemma [quot_respect]:
+lemma concat_rsp[quot_respect]:
   shows "(list_rel op \<approx> OOO op \<approx> ===> op \<approx>) concat concat"
 proof (rule fun_relI, elim pred_compE)
   fix a b ba bb