# HG changeset patch
# User haftmann
# Date 1253259323 -7200
# Node ID 43ed78ee285d9d89948b527db334df11d3bc5193
# Parent  8b3e2bc91a46dbfe46be1e44d69f39709f532a97
simplified proof

diff -r 8b3e2bc91a46 -r 43ed78ee285d src/HOL/Lambda/Eta.thy
--- a/src/HOL/Lambda/Eta.thy	Fri Sep 18 09:07:51 2009 +0200
+++ b/src/HOL/Lambda/Eta.thy	Fri Sep 18 09:35:23 2009 +0200
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Lambda/Eta.thy
-    ID:         $Id$
     Author:     Tobias Nipkow and Stefan Berghofer
     Copyright   1995, 2005 TU Muenchen
 *)
@@ -87,7 +86,6 @@
 lemma square_eta: "square eta eta (eta^==) (eta^==)"
   apply (unfold square_def id_def)
   apply (rule impI [THEN allI [THEN allI]])
-  apply simp
   apply (erule eta.induct)
      apply (slowsimp intro: subst_not_free eta_subst free_eta [THEN iffD1])
     apply safe