Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Explicitely applied ext in proof of tnd.
authorberghofe
Wed, 07 May 2008 10:59:43 +0200
changeset 26828 60d1fa8e0831
parent 26827 a62f8db42f4a
child 26829 229e8078b1e0
Explicitely applied ext in proof of tnd.
src/HOL/ex/Hilbert_Classical.thy file | annotate | diff | comparison | revisions 
--- 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"
isabelle