--- a/ex/Rec.ML Fri Nov 11 10:35:03 1994 +0100 +++ b/ex/Rec.ML Mon Nov 21 17:50:34 1994 +0100 @@ -2,4 +2,4 @@ goalw thy [mono_def,Domf_def] "mono(Domf(F))"; by (DEPTH_SOLVE (slow_step_tac set_cs 1)); -val mono_Domf = result(); +qed "mono_Domf";