diff -r 722fa927e505 -r 268a727b0f10 LamEx.thy --- 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 \ op \" 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 \ op \" 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 *)