Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Proofs/Lambda/Eta.thy
changeset 47124 960f0a4404c7
parent 39157 b98909faaea8
child 58273 9f0bfcd15097 
--- a/src/HOL/Proofs/Lambda/Eta.thy	Mon Mar 26 18:32:22 2012 +0200
+++ b/src/HOL/Proofs/Lambda/Eta.thy	Mon Mar 26 19:03:27 2012 +0200
@@ -159,7 +159,7 @@
      apply (slowsimp intro: rtrancl_eta_subst eta_subst)
     apply (blast intro: rtrancl_eta_AppL)
    apply (blast intro: rtrancl_eta_AppR)
-  apply simp;
+  apply simp
   apply (slowsimp intro: rtrancl_eta_Abs free_beta
     iff del: dB.distinct simp: dB.distinct)    (*23 seconds?*)
   done
isabelle