Nominal/Ex/Foo1.thy
changeset 2559 add799cf0817
parent 2503 cc5d23547341
child 2560 82e37a4595c7
--- a/Nominal/Ex/Foo1.thy	Wed Nov 10 13:40:46 2010 +0000
+++ b/Nominal/Ex/Foo1.thy	Wed Nov 10 13:46:21 2010 +0000
@@ -74,7 +74,7 @@
 
 lemma [quot_respect]: 
   shows "((op =) ===> alpha_assg_raw ===> alpha_assg_raw) permute_bn1_raw permute_bn1_raw"
-  apply simp
+  apply (simp add: fun_rel_def)
   apply clarify
   apply (erule alpha_assg_raw.cases)
   apply simp_all
@@ -84,7 +84,7 @@
 
 lemma [quot_respect]: 
   shows "((op =) ===> alpha_assg_raw ===> alpha_assg_raw) permute_bn2_raw permute_bn2_raw"
-  apply simp
+  apply (simp add: fun_rel_def)
   apply clarify
   apply (erule alpha_assg_raw.cases)
   apply simp_all
@@ -94,7 +94,7 @@
 
 lemma [quot_respect]: 
   shows "((op =) ===> alpha_assg_raw ===> alpha_assg_raw) permute_bn3_raw permute_bn3_raw"
-  apply simp
+  apply (simp add: fun_rel_def)
   apply clarify
   apply (erule alpha_assg_raw.cases)
   apply simp_all