diff -r 38810e1df801 -r fcff14e578d3 LamEx.thy --- 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