--- a/LamEx.thy Thu Oct 29 07:29:12 2009 +0100
+++ b/LamEx.thy Thu Oct 29 08:06:49 2009 +0100
@@ -17,7 +17,6 @@
| a3: "\<lbrakk>t \<approx> ([(a,b)]\<bullet>s); a\<sharp>[b].s\<rbrakk> \<Longrightarrow> rLam a t \<approx> rLam b s"
quotient lam = rlam / alpha
-apply -
sorry
print_quotients