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/ex/Hilbert_Classical.thy
changeset 32960 69916a850301
parent 26828 60d1fa8e0831 
--- a/src/HOL/ex/Hilbert_Classical.thy	Sat Oct 17 01:05:59 2009 +0200
+++ b/src/HOL/ex/Hilbert_Classical.thy	Sat Oct 17 14:43:18 2009 +0200
@@ -47,45 +47,45 @@
       assume Q: "Eps ?Q = True"
       have neq: "?P \<noteq> ?Q"
       proof
-	assume "?P = ?Q"
-	hence "Eps ?P = Eps ?Q" by (rule arg_cong)
-	also note P
-	also note Q
-	finally show False by (rule False_neq_True)
+        assume "?P = ?Q"
+        hence "Eps ?P = Eps ?Q" by (rule arg_cong)
+        also note P
+        also note Q
+        finally show False by (rule False_neq_True)
       qed
       have "\<not> A"
       proof
-	assume a: A
-	have "?P = ?Q"
-	proof (rule ext)
-	  fix x show "?P x = ?Q x"
-	  proof
-	    assume "?P x"
-	    thus "?Q x"
-	    proof
-	      assume "x = False"
-	      from this and a have "x = False \<and> A" ..
-	      thus "?Q x" ..
-	    next
-	      assume "x = True \<and> A"
-	      hence "x = True" ..
-	      thus "?Q x" ..
-	    qed
-	  next
-	    assume "?Q x"
-	    thus "?P x"
-	    proof
-	      assume "x = False \<and> A"
-	      hence "x = False" ..
-	      thus "?P x" ..
-	    next
-	      assume "x = True"
-	      from this and a have "x = True \<and> A" ..
-	      thus "?P x" ..
-	    qed
-	  qed
-	qed
-	with neq show False by contradiction
+        assume a: A
+        have "?P = ?Q"
+        proof (rule ext)
+          fix x show "?P x = ?Q x"
+          proof
+            assume "?P x"
+            thus "?Q x"
+            proof
+              assume "x = False"
+              from this and a have "x = False \<and> A" ..
+              thus "?Q x" ..
+            next
+              assume "x = True \<and> A"
+              hence "x = True" ..
+              thus "?Q x" ..
+            qed
+          next
+            assume "?Q x"
+            thus "?P x"
+            proof
+              assume "x = False \<and> A"
+              hence "x = False" ..
+              thus "?P x" ..
+            next
+              assume "x = True"
+              from this and a have "x = True \<and> A" ..
+              thus "?P x" ..
+            qed
+          qed
+        qed
+        with neq show False by contradiction
       qed
       thus ?thesis ..
     qed
isabelle