# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1265110561 -3600
# Node ID 559419060d99b70fa74bb58db1bb651ccb65a415
# Parent  b3deb964ad26b11affc4c095d23f32824b29554a
Minor uncommited changes from LamEx2.

diff -r b3deb964ad26 -r 559419060d99 Quot/Nominal/LamEx2.thy
--- a/Quot/Nominal/LamEx2.thy	Tue Feb 02 11:56:37 2010 +0100
+++ b/Quot/Nominal/LamEx2.thy	Tue Feb 02 12:36:01 2010 +0100
@@ -111,7 +111,7 @@
   a1: "a = b \<Longrightarrow> (rVar a) \<approx> (rVar b)"
 | a2: "\<lbrakk>t1 \<approx> t2; s1 \<approx> s2\<rbrakk> \<Longrightarrow> rApp t1 s1 \<approx> rApp t2 s2"
 | a3: "\<exists>pi. (({atom a}, t) \<approx>gen alpha rfv pi ({atom b}, s)) \<Longrightarrow> rLam a t \<approx> rLam b s"
-
+print_theorems
 thm alpha.induct
 
 lemma a3_inverse:
@@ -130,7 +130,7 @@
 apply(simp add: a2)
 apply(simp)
 apply(rule a3)
-apply(rule alpha_gen_eqvt_atom)
+apply(rule alpha_gen_atom_eqvt)
 apply(rule rfv_eqvt)
 apply assumption
 done
@@ -160,13 +160,10 @@
 lemma alpha_trans:
   shows "t1 \<approx> t2 \<Longrightarrow> t2 \<approx> t3 \<Longrightarrow> t1 \<approx> t3"
 apply(induct arbitrary: t3 rule: alpha.induct)
-apply(erule alpha.cases)
-apply(simp_all)
 apply(simp add: a1)
 apply(rotate_tac 4)
 apply(erule alpha.cases)
-apply(simp_all)
-apply(simp add: a2)
+apply(simp_all add: a2)
 apply(erule alpha.cases)
 apply(simp_all)
 apply(rule a3)