# HG changeset patch
# User berghofe
# Date 1210150783 -7200
# Node ID 60d1fa8e0831bca88104a5f2fd68f71f4e6552d3
# Parent  a62f8db42f4a47ca5640878ec034578b4333594c
Explicitely applied ext in proof of tnd.

diff -r a62f8db42f4a -r 60d1fa8e0831 src/HOL/ex/Hilbert_Classical.thy
--- a/src/HOL/ex/Hilbert_Classical.thy	Wed May 07 10:59:42 2008 +0200
+++ b/src/HOL/ex/Hilbert_Classical.thy	Wed May 07 10:59:43 2008 +0200
@@ -57,7 +57,7 @@
       proof
 	assume a: A
 	have "?P = ?Q"
-	proof
+	proof (rule ext)
 	  fix x show "?P x = ?Q x"
 	  proof
 	    assume "?P x"