Old_HOL: ex/Rec.ML@1a3d3b5b5d15 (annotated)

0 7949f97df77a Initial revision clasohm parents: diff changeset	1	open Rec;
7949f97df77a Initial revision clasohm parents: diff changeset	2
7949f97df77a Initial revision clasohm parents: diff changeset	3	goalw thy [mono_def,Domf_def] "mono(Domf(F))";
7949f97df77a Initial revision clasohm parents: diff changeset	4	by (DEPTH_SOLVE (slow_step_tac set_cs 1));
171 16c4ea954511 replaced 'val ... = result()' by 'qed "..."' clasohm parents: 0 diff changeset	5	qed "mono_Domf";