src/HOL/HOL.ML
changeset 4025 77e426be5624
parent 3842 b55686a7b22c
child 4087 42229596565c
--- 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"