Lines Matching defs:instructions
860 val instructions = ref ([] : (string * thm) list);
866 val _ = instructions := (name,thm) :: !instructions
3869 val instructions =
3872 map (I ## instruction_rule) (!instructions);
3874 val _ = map save_thm instructions;
3875 val _ = computeLib.add_persistent_funs (map fst instructions);
3877 val instructions = map fst (List.drop (instructions,2));
3882 (quote (hd instructions) ^ "]\n") (tl instructions);