1.1 --- a/etc/proofgeneral-settings.el	Fri Sep 28 19:24:25 2001 +0200
     1.2 +++ b/etc/proofgeneral-settings.el	Fri Sep 28 20:08:05 2001 +0200
     1.3 @@ -1,8 +1,12 @@
     1.4 -;
     1.5 -; $Id$
     1.6 -;
     1.7 -; Options for Proof General
     1.8 -;
     1.9 +;;;
    1.10 +;;; $Id$
    1.11 +;;;
    1.12 +;;; Options for Proof General
    1.13  
    1.14 -; Override XEmacs custom settings (commented out)
    1.15 +;; Examples for sensible settings:
    1.16 +
    1.17  ;(custom-set-variables '(isar-eta-contract nil))
    1.18 +
    1.19 +;(custom-set-faces
    1.20 +; '(proof-locked-face
    1.21 +;   ((((type x) (class color) (background light)) (:background "lightsteelblue2")))))

     2.1 --- a/src/HOL/ex/Hilbert_Classical.thy	Fri Sep 28 19:24:25 2001 +0200
     2.2 +++ b/src/HOL/ex/Hilbert_Classical.thy	Fri Sep 28 20:08:05 2001 +0200
     2.3 @@ -52,8 +52,7 @@
     2.4  	hence "Eps ?P = Eps ?Q" by (rule arg_cong)
     2.5  	also note P
     2.6  	also note Q
     2.7 -	finally have "False = True" .	
     2.8 -	thus False by (rule False_neq_True)
     2.9 +	finally show False by (rule False_neq_True)
    2.10        qed
    2.11        have "\<not> A"
    2.12        proof