ex/rec.ML
author clasohm
Wed, 02 Mar 1994 12:26:55 +0100
changeset 48 21291189b51e
parent 0 7949f97df77a
permissions -rw-r--r--
changed "." to "$" and Cons to infix "#" to eliminate ambiguity
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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));
7949f97df77a Initial revision
clasohm
parents:
diff changeset
     5
val mono_Domf = result();