changeset 4031 | 42cbf6256d60 |
parent 3842 | b55686a7b22c |
child 4098 | 71e05eb27fb6 |
--- a/src/HOLCF/Porder.ML Wed Oct 29 14:23:49 1997 +0100 +++ b/src/HOLCF/Porder.ML Wed Oct 29 16:03:19 1997 +0100 @@ -12,7 +12,7 @@ (* lubs are unique *) (* ------------------------------------------------------------------------ *) -qed_goalw "unique_lub "thy [is_lub, is_ub] +qed_goalw "unique_lub" thy [is_lub, is_ub] "[| S <<| x ; S <<| y |] ==> x=y" ( fn prems => [