src/HOLCF/Sprod2.ML
changeset 4031 42cbf6256d60
parent 3842 b55686a7b22c
child 4721 c8a8482a8124
     1.1 --- a/src/HOLCF/Sprod2.ML	Wed Oct 29 14:23:49 1997 +0100
     1.2 +++ b/src/HOLCF/Sprod2.ML	Wed Oct 29 16:03:19 1997 +0100
     1.3 @@ -66,7 +66,7 @@
     1.4          ]);
     1.5  
     1.6  
     1.7 -qed_goal " monofun_Ispair" Sprod2.thy 
     1.8 +qed_goal "monofun_Ispair" Sprod2.thy 
     1.9   "[|x1<<x2; y1<<y2|] ==> Ispair x1 y1 << Ispair x2 y2"
    1.10  (fn prems =>
    1.11          [