diff -r 99e811fc1366 -r e49c6b6f37f4 Quot/Examples/LamEx.thy --- a/Quot/Examples/LamEx.thy Thu Jan 14 19:03:08 2010 +0100 +++ b/Quot/Examples/LamEx.thy Thu Jan 14 23:17:21 2010 +0100 @@ -360,18 +360,11 @@ qed -lemma var_supp: - shows "supp (Var a) = ((supp a)::name set)" - apply(simp add: supp_def) - apply(simp add: pi_var2) - apply(simp add: var_inject) - done - lemma var_fresh: fixes a::"name" shows "(a \ (Var b)) = (a \ b)" apply(simp add: fresh_def) - apply(simp add: var_supp) + apply(simp add: var_supp1) done end