*** Failed to load theory "HOL-Imperative_HOL.Imperative_HOL_ex" (unresolved "HOL-Imperative_HOL.Imperative_Quicksort", "HOL-Imperative_HOL.Imperative_Reverse", "HOL-Imperative_HOL.Linked_Lists")
*** Code check failed for OCaml: "$ISABELLE_OCAMLFIND" ocamlopt -w pu -package zarith -linkpkg ROOT.ml </dev/null
*** At command "export_code" (line 965 of "~~/src/HOL/Imperative_HOL/ex/Linked_Lists.thy")
*** Code check failed for OCaml: "$ISABELLE_OCAMLFIND" ocamlopt -w pu -package zarith -linkpkg ROOT.ml </dev/null
*** At command "export_code" (line 667 of "~~/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy")
*** At command "by" (line 69 of "~~/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy")
*** Code check failed for OCaml: "$ISABELLE_OCAMLFIND" ocamlopt -w pu -package zarith -linkpkg ROOT.ml </dev/null
*** At command "export_code" (line 667 of "~~/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy")
*** Code check failed for OCaml: "$ISABELLE_OCAMLFIND" ocamlopt -w pu -package zarith -linkpkg ROOT.ml </dev/null
*** At command "export_code" (line 115 of "~~/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy")
*** At command "by" (line 56 of "~~/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy")
*** Code check failed for OCaml: "$ISABELLE_OCAMLFIND" ocamlopt -w pu -package zarith -linkpkg ROOT.ml </dev/null
*** At command "export_code" (line 115 of "~~/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy")