--- a/src/HOL/ex/Rec.ML Thu Jun 13 16:22:37 1996 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,5 +0,0 @@ -open Rec; - -goalw thy [mono_def,Domf_def] "mono(Domf(F))"; -by (DEPTH_SOLVE (slow_step_tac set_cs 1)); -qed "mono_Domf";