--- 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")))))
--- 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