# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1267539170 -3600
# Node ID c668d65fd98865583a7cb3f1f878aafcee209f0a
# Parent  b395b902cf0d6ca02732757fa45854ecf021dcea
Minor

diff -r b395b902cf0d -r c668d65fd988 Nominal/LFex.thy
--- a/Nominal/LFex.thy	Tue Mar 02 15:11:41 2010 +0100
+++ b/Nominal/LFex.thy	Tue Mar 02 15:12:50 2010 +0100
@@ -45,11 +45,10 @@
 done
 
 lemma alpha_eqvt:
-  "t1 \<approx>ki s1 \<Longrightarrow> (pi \<bullet> t1) \<approx>ki (pi \<bullet> s1)"
-  "t2 \<approx>ty s2 \<Longrightarrow> (pi \<bullet> t2) \<approx>ty (pi \<bullet> s2)"
-  "t3 \<approx>tr s3 \<Longrightarrow> (pi \<bullet> t3) \<approx>tr (pi \<bullet> s3)"
-apply(induct rule: alpha_rkind_alpha_rty_alpha_rtrm.inducts)
-apply (simp_all add: alpha_rkind_alpha_rty_alpha_rtrm.intros)
+  "(t1 \<approx>ki s1 \<longrightarrow> (p \<bullet> t1) \<approx>ki (p \<bullet> s1)) \<and>
+   (t2 \<approx>ty s2 \<longrightarrow> (p \<bullet> t2) \<approx>ty (p \<bullet> s2)) \<and>
+   (t3 \<approx>tr s3 \<longrightarrow> (p \<bullet> t3) \<approx>tr (p \<bullet> s3))"
+apply(rule alpha_rkind_alpha_rty_alpha_rtrm.induct)
 apply (simp_all add: alpha_rkind_alpha_rty_alpha_rtrm_inj)
 apply (erule alpha_gen_compose_eqvt)
 apply (simp_all add: rfv_eqvt eqvts atom_eqvt)