--- a/LamEx.thy	Wed Oct 28 17:38:37 2009 +0100
+++ b/LamEx.thy	Wed Oct 28 18:08:38 2009 +0100
@@ -43,9 +43,9 @@
 
 (* Construction Site code *)
 
-lemma perm_rsp: "op = ===> alpha ===> alpha op \<bullet> op \<bullet>" sorry
-lemma fresh_rsp: "op = ===> (alpha ===> op =) fresh fresh" sorry
-lemma rLam_rsp: "op = ===> (alpha ===> alpha) rLam rLam" sorry
+lemma perm_rsp: "(op = ===> alpha ===> alpha) op \<bullet> op \<bullet>" sorry
+lemma fresh_rsp: "(op = ===> (alpha ===> op =)) fresh fresh" sorry
+lemma rLam_rsp: "(op = ===> (alpha ===> alpha)) rLam rLam" sorry
 
 ML {* val defs = @{thms Var_def App_def Lam_def} *}
 ML {* val consts = [@{const_name "rVar"}, @{const_name "rApp"}, @{const_name "rLam"}]; *}
@@ -91,7 +91,4 @@
 ML {* ObjectLogic.rulify t_b' *}
 
 ML {* val t_u = MetaSimplifier.rewrite_rule @{thms fresh_def supp_def} @{thm a3} *}
-lemma "alpha ===> (alpha ===> op =) op = op ="
-sorry
-
 ML {* Toplevel.program (fn () => lift_thm_lam @{context} t_u) *} (* Is not ture *)