# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1265731507 -3600
# Node ID 84d666f9faceb48dbf9855f948d099c3c97485b2
# Parent  7e691b3c2414ba058bdbb3dbe895b2449868a876
the specifications of the respects.

diff -r 7e691b3c2414 -r 84d666f9face Quot/Nominal/Terms.thy
--- a/Quot/Nominal/Terms.thy	Tue Feb 09 16:44:06 2010 +0100
+++ b/Quot/Nominal/Terms.thy	Tue Feb 09 17:05:07 2010 +0100
@@ -1023,7 +1023,17 @@
 as
   "rbv6"
 
+lemma [quot_respect]:"(alpha6 ===> op =) rbv6 rbv6"
+apply simp apply clarify
+apply (erule alpha6.induct)
+apply simp
+apply simp
+apply (erule exE)
+apply (simp add: alpha_gen)
+sorry
 
+lemma [quot_respect]:"(alpha6 ===> op =) rfv_trm6 rfv_trm6"
+sorry
 
 lemma [quot_respect]:
  "(op = ===> alpha6) rVr6 rVr6"
@@ -1039,6 +1049,11 @@
 
 instantiation trm6 :: pt begin
 
+quotient_definition
+  "permute_trm6 :: perm \<Rightarrow> trm6 \<Rightarrow> trm6"
+as
+  "permute :: perm \<Rightarrow> rtrm6 \<Rightarrow> rtrm6"
+
 instance
 sorry
 end
@@ -1048,9 +1063,6 @@
 apply (unfold alpha_gen)
 apply (lifting a3[unfolded alpha_gen])
 apply injection
-
-
-
 sorry