# HG changeset patch
# User wenzelm
# Date 878056900 -3600
# Node ID 77e426be562413ef5bbc079464e16de49469d5d7
# Parent  3c056eab237c3328922f359ac346933b89cc1884
fixed qed;

diff -r 3c056eab237c -r 77e426be5624 src/HOL/HOL.ML
--- a/src/HOL/HOL.ML	Tue Oct 28 17:41:15 1997 +0100
+++ b/src/HOL/HOL.ML	Tue Oct 28 17:41:40 1997 +0100
@@ -77,7 +77,7 @@
 qed_goalw "TrueI" HOL.thy [True_def] "True"
   (fn _ => [rtac refl 1]);
 
-qed_goal "eqTrueI " HOL.thy "P ==> P=True" 
+qed_goal "eqTrueI" HOL.thy "P ==> P=True" 
  (fn prems => [REPEAT(resolve_tac ([iffI,TrueI]@prems) 1)]);
 
 qed_goal "eqTrueE" HOL.thy "P=True ==> P"