fixed qed;
authorwenzelm
Tue Oct 28 17:41:40 1997 +0100 (1997-10-28)
changeset 402577e426be5624
parent 4024 3c056eab237c
child 4026 b94dc94be4b7
fixed qed;
src/HOL/HOL.ML
     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"