# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1268848379 -3600
# Node ID b9caceeec805608ab2fb86482619aa6a1e36f033
# Parent  44e68ab6841eaa5098eb728bee2e5cc8760d1376
compose_sym2 works also for term5

diff -r 44e68ab6841e -r b9caceeec805 Nominal/Term5.thy
--- a/Nominal/Term5.thy	Wed Mar 17 17:59:04 2010 +0100
+++ b/Nominal/Term5.thy	Wed Mar 17 18:52:59 2010 +0100
@@ -71,6 +71,8 @@
 "(a \<approx>5 b \<longrightarrow> b \<approx>5 a) \<and>
 (x \<approx>l y \<longrightarrow> y \<approx>l x) \<and>
 (alpha_rbv5 x y \<longrightarrow> alpha_rbv5 y x)"
+apply (tactic {* symp_tac @{thm alpha_rtrm5_alpha_rlts_alpha_rbv5.induct} @{thms alpha5_inj} @{thms alpha5_eqvt} @{context} 1 *})
+(*
 apply (rule alpha_rtrm5_alpha_rlts_alpha_rbv5.induct)
 apply (simp_all add: alpha5_inj)
 apply (erule exE)
@@ -89,7 +91,7 @@
 apply (rotate_tac 6)
 apply simp
 apply (drule_tac p1="- pi" in permute_eq_iff[symmetric,THEN iffD1])
-apply (simp)
+apply (simp)*)
 done
 
 lemma alpha5_transp: