Lines Matching defs:instructions
883 val instructions = ref ([] : (string * thm) list);
889 val _ = instructions := (name,thm) :: !instructions
3892 val instructions =
3895 map (I ## instruction_rule) (!instructions);
3897 val _ = map save_thm instructions;
3898 val _ = computeLib.add_persistent_funs (map fst instructions);
3900 val instructions = map fst (List.drop (instructions,2));
3905 (quote (hd instructions) ^ "]\n") (tl instructions);