fixed spaces in qed;
authorwenzelm
Wed Oct 29 16:03:19 1997 +0100 (1997-10-29)
changeset 403142cbf6256d60
parent 4030 ca44afcc259c
child 4032 4b1c69d8b767
fixed spaces in qed;
src/HOLCF/Porder.ML
src/HOLCF/Sprod2.ML
     1.1 --- a/src/HOLCF/Porder.ML	Wed Oct 29 14:23:49 1997 +0100
     1.2 +++ b/src/HOLCF/Porder.ML	Wed Oct 29 16:03:19 1997 +0100
     1.3 @@ -12,7 +12,7 @@
     1.4  (* lubs are unique                                                          *)
     1.5  (* ------------------------------------------------------------------------ *)
     1.6  
     1.7 -qed_goalw "unique_lub "thy [is_lub, is_ub] 
     1.8 +qed_goalw "unique_lub" thy [is_lub, is_ub] 
     1.9          "[| S <<| x ; S <<| y |] ==> x=y"
    1.10  ( fn prems =>
    1.11          [
     2.1 --- a/src/HOLCF/Sprod2.ML	Wed Oct 29 14:23:49 1997 +0100
     2.2 +++ b/src/HOLCF/Sprod2.ML	Wed Oct 29 16:03:19 1997 +0100
     2.3 @@ -66,7 +66,7 @@
     2.4          ]);
     2.5  
     2.6  
     2.7 -qed_goal " monofun_Ispair" Sprod2.thy 
     2.8 +qed_goal "monofun_Ispair" Sprod2.thy 
     2.9   "[|x1<<x2; y1<<y2|] ==> Ispair x1 y1 << Ispair x2 y2"
    2.10  (fn prems =>
    2.11          [