ex/Rec.ML
author clasohm
Tue, 09 Nov 1993 13:30:13 +0100
changeset 15 25ec61ee621c
parent 0 7949f97df77a
child 171 16c4ea954511
permissions -rw-r--r--
renamed meson-test.ML to mesontest.ML, used exact theory names for use_thy

open Rec;

goalw thy [mono_def,Domf_def] "mono(Domf(F))";
by (DEPTH_SOLVE (slow_step_tac set_cs 1));
val mono_Domf = result();