src/HOL/HOL.ML
changeset 4025 77e426be5624
parent 3842 b55686a7b22c
child 4087 42229596565c
     1.1 --- a/src/HOL/HOL.ML	Tue Oct 28 17:41:15 1997 +0100
     1.2 +++ b/src/HOL/HOL.ML	Tue Oct 28 17:41:40 1997 +0100
     1.3 @@ -77,7 +77,7 @@
     1.4  qed_goalw "TrueI" HOL.thy [True_def] "True"
     1.5    (fn _ => [rtac refl 1]);
     1.6  
     1.7 -qed_goal "eqTrueI " HOL.thy "P ==> P=True" 
     1.8 +qed_goal "eqTrueI" HOL.thy "P ==> P=True" 
     1.9   (fn prems => [REPEAT(resolve_tac ([iffI,TrueI]@prems) 1)]);
    1.10  
    1.11  qed_goal "eqTrueE" HOL.thy "P=True ==> P"