Lines Matching defs:defs
13 val defs = map DEFN [S_THM, K_THM, I_THM, W_THM, C_THM, o_THM, APPLY_UPDATE_THM]
15 val _ = eSML "combin" defs;
16 val _ = eCAML "combin" defs;
20 val defs =
23 val _ = eSML "pair" defs;
24 val _ = eCAML "pair" defs;
72 val defs = map DEFN
93 :: (defs @
313 @ defs
419 val defs =
466 :: defs
498 defs)
509 val defs =
514 (MLSIGSTRUCT ["datatype option = datatype Option.option"] @ defs);
516 val _ = eCAML "option" defs;
529 val defs =
537 defs);
539 val _ = eCAML "basicSize" (MLSIGSTRUCT ["type num = NumML.num"] @ defs);
591 val defs =
604 defs)
611 defs)
689 val defs =
700 :: defs)
706 :: defs)
731 val defs =
764 :: defs)
852 val defs =
872 :: defs)
880 :: defs)
903 val defs =
907 val _ = eSML "sum" defs
908 val _ = eCAML "sum" defs;
1061 val defs =
1079 defs)
1084 defs)
1109 val defs = [SUMi, MULi, EXPi, dimindexi, mk_fcp_def, index_comp, fcp_subst_comp]
1118 map DEFN defs)
1127 :: map (DEFN o REWRITE_RULE [GSYM FCPi_def, FUN_EQ_THM]) defs)
1241 fun defs ocaml =
1275 :: defs false)
1286 defs true)
1504 val defs =
1507 val _ = eSML "sorting" defs;
1508 val _ = eCAML "sorting" defs;