# HG changeset patch
# User wenzelm
# Date 1001700485 -7200
# Node ID fd242f857508881dfe273bd9a9b2dbd7d57ad5dd
# Parent  cddf6441a14adbf6ef6bee197ae521b2a265f26e
tuned;

diff -r cddf6441a14a -r fd242f857508 etc/proofgeneral-settings.el
--- a/etc/proofgeneral-settings.el	Fri Sep 28 19:24:25 2001 +0200
+++ b/etc/proofgeneral-settings.el	Fri Sep 28 20:08:05 2001 +0200
@@ -1,8 +1,12 @@
-;
-; $Id$
-;
-; Options for Proof General
-;
+;;;
+;;; $Id$
+;;;
+;;; Options for Proof General
 
-; Override XEmacs custom settings (commented out)
+;; Examples for sensible settings:
+
 ;(custom-set-variables '(isar-eta-contract nil))
+
+;(custom-set-faces
+; '(proof-locked-face
+;   ((((type x) (class color) (background light)) (:background "lightsteelblue2")))))
diff -r cddf6441a14a -r fd242f857508 src/HOL/ex/Hilbert_Classical.thy
--- a/src/HOL/ex/Hilbert_Classical.thy	Fri Sep 28 19:24:25 2001 +0200
+++ b/src/HOL/ex/Hilbert_Classical.thy	Fri Sep 28 20:08:05 2001 +0200
@@ -52,8 +52,7 @@
 	hence "Eps ?P = Eps ?Q" by (rule arg_cong)
 	also note P
 	also note Q
-	finally have "False = True" .	
-	thus False by (rule False_neq_True)
+	finally show False by (rule False_neq_True)
       qed
       have "\<not> A"
       proof