had some fun writing an IsabelleHOL backend

(do not actually use this, most things are broken, and the primitives
lib barely exists and is simply incorrect. But it is enough to create
syntax-correct Isabelle code for relatively simply rust code, as long
as it does not contain any uses of traits)

9 files changed, 440 insertions, 132 deletions

diff --git a/compiler/Config.ml b/compiler/Config.ml
index 98a5eea1..0abe94a9 100644
--- a/compiler/Config.ml
+++ b/compiler/Config.ml
@@ -3,9 +3,9 @@
 (** {1 Backend choice} *)
 
 (** The choice of backend *)
-type backend = FStar | Coq | Lean | HOL4
+type backend = FStar | Coq | Lean | HOL4 | IsabelleHOL
 
-let backend_names = [ "fstar"; "coq"; "lean"; "hol4" ]
+let backend_names = [ "fstar"; "coq"; "lean"; "hol4"; "IsabelleHOL"]
 
 (** Utility to compute the backend from an input parameter *)
 let backend_of_string (b : string) : backend option =
@@ -14,6 +14,7 @@ let backend_of_string (b : string) : backend option =
   | "coq" -> Some Coq
   | "lean" -> Some Lean
   | "hol4" -> Some HOL4
+  | "IsabelleHOL" -> Some IsabelleHOL
   | _ -> None
 
 let opt_backend : backend option ref = ref None
@@ -374,7 +375,7 @@ let variant_concatenate_type_name = ref true
 let use_tuple_structs = ref true
 
 let backend_has_tuple_projectors backend =
-  match backend with Lean -> true | Coq | FStar | HOL4 -> false
+  match backend with Lean -> true | Coq | FStar | HOL4 | IsabelleHOL -> false
 
 (** Toggle the use of tuple projectors *)
 let use_tuple_projectors = ref false
diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index cf632388..e640edd1 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -62,6 +62,7 @@ let extract_fun_decl_register_names (ctx : extraction_ctx)
               match backend () with
               | Coq | FStar -> ctx
               | HOL4 -> craise __FILE__ __LINE__ def.item_meta.span "Unexpected"
+              | IsabelleHOL -> craise __FILE__ __LINE__ def.item_meta.span "Unexpected"
               | Lean -> ctx_add_decreases_proof def ctx
             else ctx
           in
@@ -280,7 +281,7 @@ let lets_require_wrap_in_do (span : Meta.span)
   | Lean ->
       (* For Lean, we wrap in a block iff at least one of the let-bindings is monadic *)
       List.exists (fun (m, _, _) -> m) lets
-  | HOL4 ->
+  | HOL4 | IsabelleHOL ->
       (* HOL4 is similar to HOL4, but we add a sanity check *)
       let wrap_in_do = List.exists (fun (m, _, _) -> m) lets in
       if wrap_in_do then
@@ -305,7 +306,7 @@ let extract_texpression_errors (fmt : F.formatter) =
   match backend () with
   | FStar | Coq -> F.pp_print_string fmt "admit"
   | Lean -> F.pp_print_string fmt "sorry"
-  | HOL4 -> F.pp_print_string fmt "(* ERROR: could not generate the code *)"
+  | HOL4 | IsabelleHOL -> F.pp_print_string fmt "(* ERROR: could not generate the code *)"
 
 let rec extract_texpression (span : Meta.span) (ctx : extraction_ctx)
     (fmt : F.formatter) (inside : bool) (e : texpression) : unit =
@@ -596,7 +597,7 @@ and extract_field_projector (span : Meta.span) (ctx : extraction_ctx)
           (* Check if we need to extract the type as a tuple *)
           if is_tuple_struct then
             match backend () with
-            | FStar | HOL4 | Coq -> FieldId.to_string proj.field_id
+            | FStar | HOL4 | Coq | IsabelleHOL -> FieldId.to_string proj.field_id
             | Lean ->
                 (* Tuples in Lean are syntax sugar for nested products/pairs,
                    so we need to map the field id accordingly.
@@ -644,15 +645,24 @@ and extract_field_projector (span : Meta.span) (ctx : extraction_ctx)
         in
         (* Open a box *)
         F.pp_open_hovbox fmt ctx.indent_incr;
-        (* Extract the expression *)
-        extract_texpression span ctx fmt true arg;
-        (* We allow to break where the "." appears (except Lean, it's a syntax error) *)
-        if backend () <> Lean then F.pp_print_break fmt 0 0;
-        F.pp_print_string fmt ".";
-        (* If in Coq, the field projection has to be parenthesized *)
-        (match backend () with
-        | FStar | Lean | HOL4 -> F.pp_print_string fmt field_name
-        | Coq -> F.pp_print_string fmt ("(" ^ field_name ^ ")"));
+        (* In Isabelle, there is no special record syntax, so fake a function call *)
+        if backend () = IsabelleHOL then (
+          if inside then F.pp_print_string fmt "(";
+          F.pp_print_string fmt field_name;
+          F.pp_print_space fmt ();
+          extract_texpression span ctx fmt true arg;
+          if inside then F.pp_print_string fmt ")")
+        else (
+          (* Extract the expression *)
+          extract_texpression span ctx fmt true arg;
+          (* We allow to break where the "." appears (except Lean, it's a syntax error) *)
+          if backend () <> Lean then F.pp_print_break fmt 0 0;
+          F.pp_print_string fmt ".";
+          (* If in Coq, the field projection has to be parenthesized *)
+          (match backend () with
+          | FStar | Lean | HOL4 | IsabelleHOL -> F.pp_print_string fmt field_name
+          | Coq -> F.pp_print_string fmt ("(" ^ field_name ^ ")"));
+        );
         (* Close the box *)
         F.pp_close_box fmt ()
   | arg :: args ->
@@ -718,7 +728,7 @@ and extract_lets (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter)
   let lets, next_e =
     match backend () with
     | HOL4 -> destruct_lets_no_interleave span e
-    | FStar | Coq | Lean -> destruct_lets e
+    | FStar | Coq | Lean | IsabelleHOL -> destruct_lets e
   in
   (* Extract the let-bindings *)
   let extract_let (ctx : extraction_ctx) (monadic : bool) (lv : typed_pattern)
@@ -743,7 +753,7 @@ and extract_lets (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter)
         let arrow =
           match backend () with
           | Coq | HOL4 -> "<-"
-          | FStar | Lean -> craise __FILE__ __LINE__ span "impossible"
+          | FStar | Lean | IsabelleHOL -> craise __FILE__ __LINE__ span "impossible"
         in
         F.pp_print_string fmt arrow;
         F.pp_print_space fmt ();
@@ -760,7 +770,7 @@ and extract_lets (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter)
           | Coq | Lean ->
               F.pp_print_string fmt "let";
               F.pp_print_space fmt ()
-          | HOL4 -> ()
+          | HOL4 | IsabelleHOL -> ()
         else (
           F.pp_print_string fmt "let";
           F.pp_print_space fmt ());
@@ -772,6 +782,7 @@ and extract_lets (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter)
           | Coq -> ":="
           | Lean -> if monadic then "←" else ":="
           | HOL4 -> if monadic then "<-" else "="
+          | IsabelleHOL -> if monadic then "\\<leftarrow>" else "="
         in
         F.pp_print_string fmt eq;
         F.pp_print_space fmt ();
@@ -783,7 +794,13 @@ and extract_lets (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter)
             ()
         | Coq | FStar | HOL4 ->
             F.pp_print_space fmt ();
-            F.pp_print_string fmt "in");
+            F.pp_print_string fmt "in";
+        | IsabelleHOL ->
+          if monadic then
+            F.pp_print_string fmt ";"
+          else (
+            F.pp_print_space fmt ();
+            F.pp_print_string fmt "in"));
         ctx)
     in
     (* Close the box for the let-binding *)
@@ -798,7 +815,10 @@ and extract_lets (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter)
      at the end of every let-binding: let-bindings are indeed not ended
      with an "in" keyword.
   *)
-  if backend () = Lean then F.pp_open_vbox fmt 0 else F.pp_open_hvbox fmt 0;
+  if backend () = Lean then
+    F.pp_open_vbox fmt 0
+  else
+    F.pp_open_hvbox fmt (if backend () = IsabelleHOL then ctx.indent_incr else 0);
   (* Open parentheses *)
   if inside && backend () <> Lean then F.pp_print_string fmt "(";
   (* If Lean and HOL4, we rely on monadic blocks, so we insert a do and open a new box
@@ -806,6 +826,8 @@ and extract_lets (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter)
   let wrap_in_do_od = lets_require_wrap_in_do span lets in
   if wrap_in_do_od then (
     F.pp_print_string fmt "do";
+    if backend () = IsabelleHOL then (
+      F.pp_print_string fmt " {");
     F.pp_print_space fmt ());
   let ctx =
     List.fold_left
@@ -820,10 +842,13 @@ and extract_lets (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter)
   F.pp_close_box fmt ();
 
   (* do-box (Lean and HOL4 only) *)
-  if wrap_in_do_od then
+  if wrap_in_do_od then (
     if backend () = HOL4 then (
       F.pp_print_space fmt ();
       F.pp_print_string fmt "od");
+    if backend () = IsabelleHOL then (
+      F.pp_print_space fmt ();
+      F.pp_print_string fmt "}"));
   (* Close parentheses *)
   if inside && backend () <> Lean then F.pp_print_string fmt ")";
   (* Close the box for the whole expression *)
@@ -845,6 +870,8 @@ and extract_Switch (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter)
   | If (e_then, e_else) ->
       (* Open a box for the [if e] *)
       F.pp_open_hovbox fmt ctx.indent_incr;
+      if backend () = IsabelleHOL then
+        F.pp_print_string fmt "(";
       F.pp_print_string fmt "if";
       if backend () = Lean && ctx.use_dep_ite then F.pp_print_string fmt " h:";
       F.pp_print_space fmt ();
@@ -875,7 +902,7 @@ and extract_Switch (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter)
                 F.pp_print_space fmt ();
                 F.pp_print_string fmt "begin";
                 F.pp_print_space fmt
-            | Coq | Lean | HOL4 ->
+            | Coq | Lean | HOL4 | IsabelleHOL ->
                 F.pp_print_space fmt ();
                 F.pp_print_string fmt "(";
                 F.pp_print_cut fmt)
@@ -896,13 +923,15 @@ and extract_Switch (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter)
            | FStar ->
                F.pp_print_space fmt ();
                F.pp_print_string fmt "end"
-           | Coq | Lean | HOL4 -> F.pp_print_string fmt ")");
+           | Coq | Lean | HOL4 | IsabelleHOL -> F.pp_print_string fmt ")");
         (* Close the box for the then/else+branch *)
         F.pp_close_box fmt ()
       in
 
       extract_branch true e_then;
-      extract_branch false e_else
+      extract_branch false e_else;
+      if backend () = IsabelleHOL then
+        F.pp_print_string fmt ")"
   | Match branches -> (
       (* Open a box for the [match ... with] *)
       F.pp_open_hovbox fmt ctx.indent_incr;
@@ -912,7 +941,7 @@ and extract_Switch (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter)
         | FStar -> "begin match"
         | Coq -> "match"
         | Lean -> if ctx.use_dep_ite then "match h:" else "match"
-        | HOL4 ->
+        | HOL4 | IsabelleHOL ->
             (* We're being extra safe in the case of HOL4 *)
             "(case"
       in
@@ -924,12 +953,15 @@ and extract_Switch (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter)
       extract_texpression span ctx fmt scrut_inside scrut;
       F.pp_print_space fmt ();
       let match_scrut_end =
-        match backend () with FStar | Coq | Lean -> "with" | HOL4 -> "of"
+        match backend () with FStar | Coq | Lean -> "with" | HOL4 | IsabelleHOL -> "of"
       in
       F.pp_print_string fmt match_scrut_end;
       (* Close the box for the [match ... with] *)
       F.pp_close_box fmt ();
 
+      let
+        first = ref true;
+      in
       (* Extract the branches *)
       let extract_branch (br : match_branch) : unit =
         F.pp_print_space fmt ();
@@ -938,12 +970,16 @@ and extract_Switch (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter)
         (* Open a box for the pattern *)
         F.pp_open_hovbox fmt ctx.indent_incr;
         (* Print the pattern *)
-        F.pp_print_string fmt "|";
+        if not !first && backend () = IsabelleHOL then
+          F.pp_print_string fmt "|"
+        else
+          F.pp_print_space fmt ();
+          first := false;
         F.pp_print_space fmt ();
         let ctx = extract_typed_pattern span ctx fmt false false br.pat in
         F.pp_print_space fmt ();
         let arrow =
-          match backend () with FStar -> "->" | Coq | Lean | HOL4 -> "=>"
+          match backend () with FStar -> "->" | Coq | Lean | HOL4 -> "=>" | IsabelleHOL -> "\\<Rightarrow>"
         in
         F.pp_print_string fmt arrow;
         (* Close the box for the pattern *)
@@ -956,7 +992,7 @@ and extract_Switch (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter)
         (* Close the box for the branch *)
         F.pp_close_box fmt ();
         (* Close the box for the pattern+branch *)
-        F.pp_close_box fmt ()
+        F.pp_close_box fmt ();
       in
 
       List.iter extract_branch branches;
@@ -967,7 +1003,7 @@ and extract_Switch (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter)
       | FStar | Coq ->
           F.pp_print_space fmt ();
           F.pp_print_string fmt "end"
-      | HOL4 -> F.pp_print_string fmt ")"));
+      | HOL4 | IsabelleHOL -> F.pp_print_string fmt ")"));
   (* Close the box for the whole expression *)
   F.pp_close_box fmt ()
 
@@ -1019,13 +1055,14 @@ and extract_StructUpdate (span : Meta.span) (ctx : extraction_ctx)
           match backend () with
           | Lean | FStar -> (Some "{", Some "}")
           | Coq -> (Some "{|", Some "|}")
-          | HOL4 -> (None, None)
+          | HOL4 | IsabelleHOL -> (None, None)
         in
         (* Inner brackets *)
         let ilb, irb =
           match backend () with
           | Lean | FStar | Coq -> (None, None)
           | HOL4 -> (Some "<|", Some "|>")
+          | IsabelleHOL -> (Some "\\<lparr>", Some "\\<rparr>")
         in
         (* Helper *)
         let print_bracket (is_left : bool) b =
@@ -1037,22 +1074,25 @@ and extract_StructUpdate (span : Meta.span) (ctx : extraction_ctx)
           | None -> ()
         in
         print_bracket true olb;
-        let need_paren = inside && backend () = HOL4 in
+        let need_paren = inside && backend () = HOL4 || backend () = IsabelleHOL in
         if need_paren then F.pp_print_string fmt "(";
         F.pp_open_hvbox fmt ctx.indent_incr;
         if supd.init <> None then (
           let var_name = ctx_get_var span (Option.get supd.init) ctx in
           F.pp_print_string fmt var_name;
           F.pp_print_space fmt ();
-          F.pp_print_string fmt "with";
-          F.pp_print_space fmt ());
+          if backend () <> IsabelleHOL then (
+            F.pp_print_string fmt "with";
+            F.pp_print_space fmt ()));
         print_bracket true ilb;
         F.pp_open_hvbox fmt 0;
         let delimiter =
-          match backend () with Lean -> "," | Coq | FStar | HOL4 -> ";"
+          match backend () with Lean | IsabelleHOL -> "," | Coq | FStar | HOL4 -> ";"
         in
         let assign =
-          match backend () with Coq | Lean | HOL4 -> ":=" | FStar -> "="
+          match backend () with
+          | Coq | Lean | HOL4 | FStar -> "="
+          | IsabelleHOL -> if supd.init <> None then ":=" else "="
         in
         Collections.List.iter_link
           (fun () ->
@@ -1100,7 +1140,7 @@ and extract_StructUpdate (span : Meta.span) (ctx : extraction_ctx)
         F.pp_close_box fmt ();
         (* Print the values *)
         let delimiter =
-          match backend () with Lean -> "," | Coq | FStar | HOL4 -> ";"
+          match backend () with Lean -> "," | Coq | FStar | HOL4 | IsabelleHOL -> ";"
         in
         F.pp_print_space fmt ();
         F.pp_open_hovbox fmt 0;
@@ -1179,16 +1219,18 @@ let extract_fun_parameters (space : bool ref) (ctx : extraction_ctx)
             insert_req_space fmt space;
             (* Open a box for the input parameter *)
             F.pp_open_hovbox fmt 0;
-            F.pp_print_string fmt "(";
+            if backend () <> IsabelleHOL then
+              F.pp_print_string fmt "(";
             let ctx =
               extract_typed_pattern def.item_meta.span ctx fmt true false lv
             in
-            F.pp_print_space fmt ();
-            F.pp_print_string fmt ":";
-            F.pp_print_space fmt ();
-            extract_ty def.item_meta.span ctx fmt TypeDeclId.Set.empty false
-              lv.ty;
-            F.pp_print_string fmt ")";
+            if backend () <> IsabelleHOL then (
+              F.pp_print_space fmt ();
+              F.pp_print_string fmt ":";
+              F.pp_print_space fmt ();
+              extract_ty def.item_meta.span ctx fmt TypeDeclId.Set.empty false
+                lv.ty;
+              F.pp_print_string fmt ")");
             (* Close the box for the input parameters *)
             F.pp_close_box fmt ();
             ctx)
@@ -1597,9 +1639,13 @@ let extract_fun_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
     F.pp_close_box fmt ()
   in
   (* Print the "=" *)
+  if backend () = IsabelleHOL then (
+    F.pp_print_space fmt ();
+    F.pp_print_string fmt "where \"";
+    F.pp_print_string fmt def_name);
   if not is_opaque then (
     F.pp_print_space fmt ();
-    let eq = match backend () with FStar | HOL4 -> "=" | Coq | Lean -> ":=" in
+    let eq = match backend () with FStar | HOL4 | IsabelleHOL -> "=" | Coq | Lean -> ":=" in
     F.pp_print_string fmt eq);
   (* Close the box for "(PARAMS) : EFFECT =" *)
   F.pp_close_box fmt ();
@@ -1704,6 +1750,128 @@ let extract_fun_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
   if backend () <> HOL4 || decl_is_not_last_from_group kind then
     F.pp_print_break fmt 0 0
 
+
+(** Extract a function definition for Isabelle/HOL. Written as its own
+    function since the syntax is a little more different from the others *)
+let extract_fun_decl_isabelle (ctx : extraction_ctx) (fmt : F.formatter)
+    (kind : decl_kind) (has_decreases_clause : bool) (def : fun_decl) : unit =
+  sanity_check __FILE__ __LINE__
+    (not def.is_global_decl_body)
+    def.item_meta.span;
+  (* Retrieve the function name *)
+  let def_name = ctx_get_local_function def.item_meta.span def.def_id def.loop_id ctx in
+  (* Add a break before *)
+  F.pp_print_break fmt 0 0;
+  (* Print a comment to link the extracted definition to its original rust definition *)
+  extract_fun_comment ctx fmt def;
+  F.pp_print_space fmt ();
+  (* Open two boxes for the definition, so that whenever possible it gets printed on
+   * one line and indents are correct *)
+  F.pp_open_hvbox fmt 0;
+  F.pp_open_vbox fmt ctx.indent_incr;
+
+  (* Open a box for "let FUN_NAME (PARAMS) : EFFECT =" *)
+  F.pp_open_vbox fmt ctx.indent_incr;
+
+  (* > "fun FUN_NAME" *)
+  (* Open a box for the "function FUN_NAME :: FUN_TYPE where" *)
+  F.pp_open_hovbox fmt ctx.indent_incr;
+
+  (* Print the top-level command *)
+  if def.signature.inputs = [] then (
+    (* functions must have at least one argument; if we have non, use definition *)
+    F.pp_print_string fmt "definition";
+    F.pp_print_space fmt ())
+  else if Option.is_some def.loop_id then (
+    (* Isabelle has "fun" and "function", which requires an explicit termination proof;
+       "fun" can prove most things, but struggles with loops, so these get a blanket
+       explicit proof
+     *)
+    F.pp_print_string fmt "function";
+    F.pp_print_space fmt ())
+  else (
+    let qualif = fun_decl_kind_to_qualif kind in
+    (match qualif with
+    | Some qualif ->
+        F.pp_print_string fmt qualif;
+        F.pp_print_space fmt ()
+    | None -> ()));
+  F.pp_print_string fmt def_name;
+  F.pp_print_space fmt ();
+
+  (* Open a box for the :: FUN_TYPE *)
+  F.pp_open_hvbox fmt 0;
+
+  (* print the function's type. TODO: this is in the wrong order;
+     the context still lacks some type variables, so this currently
+     breaks traits / sort constraints
+  *)
+  let _ =
+    (* Open a box for the return type *)
+    F.pp_open_hbox fmt ();
+    F.pp_print_string fmt "::";
+    F.pp_print_space fmt ();
+    F.pp_print_string fmt "\"";
+    (* Print the return type *)
+    (* For opaque definitions, as we don't have named parameters under the hand,
+    * we don't print parameters in the form [(x : a) (y : b) ...] above,
+    * but wait until here to print the types: [a -> b -> ...]. *)
+    extract_fun_input_parameters_types ctx fmt def;
+    (* [Tot] *)
+    if has_decreases_clause then (
+      assert_backend_supports_decreases_clauses def.item_meta.span);
+    extract_ty def.item_meta.span ctx fmt TypeDeclId.Set.empty has_decreases_clause
+      def.signature.output;
+    (* Close the box for the return type *)
+    F.pp_print_string fmt "\"";
+    F.pp_close_box fmt ();
+  in
+  (* Close the box for ":: FUN_TYPE" *)
+  F.pp_close_box fmt ();
+  F.pp_print_string fmt " where";
+  (* Close the box for the "function FUN_NAME :: FUN_TYPE where" *)
+  F.pp_close_box fmt ();
+  F.pp_print_space fmt ();
+  (* Close the box for "let FUN_NAME (PARAMS) : EFFECT =" *)
+  F.pp_close_box fmt ();
+
+  (* Open a box for the body *)
+  F.pp_open_hovbox fmt ctx.indent_incr;
+  (* Open a box for the parameters *)
+  F.pp_open_hbox fmt ();
+  F.pp_print_string fmt "\"";
+  F.pp_print_string fmt def_name;
+  let ctx, ctx_body, all_params = extract_fun_parameters (ref false) ctx fmt def in
+  F.pp_print_string fmt " =";
+  (* Close the box for the parameters *)
+  F.pp_close_box fmt ();
+  F.pp_print_space fmt ();
+
+  (* Extract the body *)
+  let _ =
+    extract_texpression def.item_meta.span ctx_body fmt false (Option.get def.body).body
+  in
+  (* Close the box for the body *)
+  F.pp_close_box fmt ();
+  (* Close the inner box for the definition *)
+  F.pp_close_box fmt ();
+  (* Close the quote of the function equation *)
+  F.pp_print_string fmt "\"";
+  (* Termination clause and proof for Lean *)
+
+  (* Close the outer box for the definition *)
+  F.pp_close_box fmt ();
+
+  (* if a loop, add a by-auto clause and hope it's enough *)
+  if Option.is_some def.loop_id then
+    F.pp_print_string fmt "  by auto";
+
+  (* Add breaks to insert new lines between definitions *)
+  (* if decl_is_not_last_from_group kind then *)
+  F.pp_print_break fmt 0 0
+
+
+
 (** Extract an opaque function declaration to HOL4.
 
     Remark (SH): having to treat this specific case separately is very annoying,
@@ -1771,6 +1939,8 @@ let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter)
   (* We treat HOL4 opaque functions in a specific manner *)
   if backend () = HOL4 && Option.is_none def.body then
     extract_fun_decl_hol4_opaque ctx fmt def
+  else if backend () = IsabelleHOL then
+    extract_fun_decl_isabelle ctx fmt kind has_decreases_clause def
   else extract_fun_decl_gen ctx fmt kind has_decreases_clause def
 
 (** Extract a global declaration body of the shape "QUALIF NAME : TYPE = BODY"
@@ -1833,7 +2003,7 @@ let extract_global_decl_body_gen (span : Meta.span) (ctx : extraction_ctx)
   if not is_opaque then (
     (* Print " =" *)
     F.pp_print_space fmt ();
-    let eq = match backend () with FStar | HOL4 -> "=" | Coq | Lean -> ":=" in
+    let eq = match backend () with FStar | HOL4 | IsabelleHOL -> "=" | Coq | Lean -> ":=" in
     F.pp_print_string fmt eq);
   (* Close ": TYPE =" box (depth=2) *)
   F.pp_close_box fmt ();
@@ -1998,6 +2168,11 @@ let extract_global_decl_aux (ctx : extraction_ctx) (fmt : F.formatter)
                        F.pp_print_string fmt "get_return_value";
                        F.pp_print_space fmt ()),
                      fun () -> () )
+               | IsabelleHOL ->
+                   ( (fun () ->
+                       F.pp_print_string fmt "value";
+                       F.pp_print_space fmt ()),
+                     fun () -> () )
              in
              before ();
              if use_brackets then F.pp_print_string fmt "(";
@@ -2305,12 +2480,16 @@ let extract_trait_item (ctx : extraction_ctx) (fmt : F.formatter)
     (item_name : string) (separator : string) (ty : unit -> unit) : unit =
   F.pp_print_space fmt ();
   F.pp_open_hovbox fmt ctx.indent_incr;
+  if backend () = IsabelleHOL then F.pp_print_string fmt "(";
   F.pp_print_string fmt item_name;
   F.pp_print_space fmt ();
   (* ":" or "=" *)
   F.pp_print_string fmt separator;
   ty ();
-  (match backend () with Lean -> () | _ -> F.pp_print_string fmt ";");
+  (match backend () with
+   | Lean -> ()
+   | IsabelleHOL -> F.pp_print_string fmt ")"
+   | _ -> F.pp_print_string fmt ";");
   F.pp_close_box fmt ()
 
 let extract_trait_decl_item (ctx : extraction_ctx) (fmt : F.formatter)
@@ -2366,7 +2545,7 @@ let extract_trait_decl_method_items (ctx : extraction_ctx) (fmt : F.formatter)
         f.signature.llbc_generics generics ctx
     in
     let backend_uses_forall =
-      match backend () with Coq | Lean -> true | FStar | HOL4 -> false
+      match backend () with Coq | Lean -> true | FStar | HOL4 | IsabelleHOL -> false
     in
     let generics_not_empty = generics <> empty_generic_params in
     let use_forall = generics_not_empty && backend_uses_forall in
@@ -2457,6 +2636,9 @@ let extract_trait_decl (ctx : extraction_ctx) (fmt : F.formatter)
           ctx_get_trait_constructor decl.item_meta.span decl.def_id ctx
         in
         F.pp_print_string fmt (":= " ^ cons ^ " {")
+    | IsabelleHOL ->
+        let cons = ctx_get_trait_constructor decl.item_meta.span decl.def_id ctx in
+        F.pp_print_string fmt ("= " ^ cons)
     | _ -> F.pp_print_string fmt "{");
 
     (* Close the box for the name + generics *)
@@ -2533,7 +2715,7 @@ let extract_trait_decl (ctx : extraction_ctx) (fmt : F.formatter)
     if backend () <> Lean then F.pp_close_box fmt ();
     (* Close the brackets *)
     match backend () with
-    | Lean -> ()
+    | Lean | IsabelleHOL -> ()
     | Coq ->
         F.pp_print_space fmt ();
         F.pp_print_string fmt "}."
@@ -2985,6 +3167,17 @@ let extract_unit_test_if_unit_fun (ctx : extraction_ctx) (fmt : F.formatter)
         if sg.inputs <> [] then (
           F.pp_print_space fmt ();
           F.pp_print_string fmt "()");
+        F.pp_print_string fmt "”)";
+    | IsabelleHOL ->
+        F.pp_print_string fmt "val _ = test_the_thing (";
+        F.pp_print_string fmt "“";
+        let fun_name =
+          ctx_get_local_function def.item_meta.span def.def_id def.loop_id ctx
+        in
+        F.pp_print_string fmt fun_name;
+        if sg.inputs <> [] then (
+          F.pp_print_space fmt ();
+          F.pp_print_string fmt "()");
         F.pp_print_string fmt "”)");
     (* Close the box for the test *)
     F.pp_close_box fmt ();
diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index 4d05f0d0..710009c4 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -512,7 +512,7 @@ let str_name () = if backend () = Lean then "String" else "string"
 let int_name (int_ty : integer_type) : string =
   let isize, usize, i_format, u_format =
     match backend () with
-    | FStar | Coq | HOL4 ->
+    | FStar | Coq | HOL4 | IsabelleHOL ->
         ("isize", "usize", format_of_string "i%d", format_of_string "u%d")
     | Lean -> ("Isize", "Usize", format_of_string "I%d", format_of_string "U%d")
   in
@@ -534,9 +534,9 @@ let scalar_name (ty : literal_type) : string =
   match ty with
   | TInteger ty -> int_name ty
   | TBool -> (
-      match backend () with FStar | Coq | HOL4 -> "bool" | Lean -> "Bool")
+      match backend () with FStar | Coq | HOL4 | IsabelleHOL -> "bool" | Lean -> "Bool")
   | TChar -> (
-      match backend () with FStar | Coq | HOL4 -> "char" | Lean -> "Char")
+      match backend () with FStar | Coq | HOL4 | IsabelleHOL -> "char" | Lean -> "Char")
 
 (** Extraction context.
 
@@ -799,7 +799,8 @@ let unop_name (unop : unop) : string =
       | FStar -> "not"
       | Lean -> "¬"
       | Coq -> "negb"
-      | HOL4 -> "~")
+      | HOL4 -> "~"
+      | IsabelleHOL -> "\\<not>")
   | Neg (int_ty : integer_type) -> (
       match backend () with Lean -> "-." | _ -> int_name int_ty ^ "_neg")
   | Cast _ ->
@@ -832,7 +833,7 @@ let named_binop_name (binop : E.binop) (int_ty : integer_type) : string =
   (* Remark: the Lean case is actually not used *)
   match backend () with
   | Lean -> int_name int_ty ^ "." ^ binop_s
-  | FStar | Coq | HOL4 -> int_name int_ty ^ "_" ^ binop_s
+  | FStar | Coq | HOL4 | IsabelleHOL -> int_name int_ty ^ "_" ^ binop_s
 
 (** A list of keywords/identifiers used by the backend and with which we
     want to check collision.
@@ -1047,6 +1048,32 @@ let keywords () =
           "then";
           "Theorem";
         ]
+    | IsabelleHOL ->
+        [
+          "axiomatization";
+          "case";
+          "definition";
+          "else";
+          "end";
+          "fix";
+          "function";
+          "fun";
+          "if";
+          "in";
+          "int";
+          "inductive";
+          "let";
+          "of";
+          "proof";
+          "lemma";
+          "qed";
+          "then";
+          "theorem";
+          "extract";
+          "o";
+          "value"
+          (* TODO: this list is very incomplete, and ironically probably contains things which aren't keywords *)
+        ]
   in
   List.concat [ named_unops; named_binops; misc ]
 
@@ -1055,7 +1082,7 @@ let assumed_adts () : (assumed_ty * string) list =
     if !use_state then
       match backend () with
       | Lean -> [ (TState, "State") ]
-      | Coq | FStar | HOL4 -> [ (TState, "state") ]
+      | Coq | FStar | HOL4 | IsabelleHOL -> [ (TState, "state") ]
     else []
   in
   (* We voluntarily omit the type [Error]: it is never directly
@@ -1073,7 +1100,7 @@ let assumed_adts () : (assumed_ty * string) list =
           (TRawPtr Mut, "MutRawPtr");
           (TRawPtr Const, "ConstRawPtr");
         ]
-    | Coq | FStar | HOL4 ->
+    | Coq | FStar | HOL4 | IsabelleHOL ->
         [
           (TResult, "result");
           (TFuel, if backend () = HOL4 then "num" else "nat");
@@ -1092,6 +1119,7 @@ let assumed_struct_constructors () : (assumed_ty * string) list =
   | Coq -> [ (TArray, "mk_array") ]
   | FStar -> [ (TArray, "mk_array") ]
   | HOL4 -> [ (TArray, "mk_array") ]
+  | IsabelleHOL -> [ (TArray, "mk_array") ]
 
 let assumed_variants () : (assumed_ty * VariantId.id * string) list =
   match backend () with
@@ -1132,10 +1160,19 @@ let assumed_variants () : (assumed_ty * VariantId.id * string) list =
         (* No Fuel::Zero on purpose *)
         (* No Fuel::Succ on purpose *)
       ]
+  | IsabelleHOL ->
+      [
+        (TResult, result_ok_id, "Ok");
+        (TResult, result_fail_id, "Fail");
+        (TError, error_failure_id, "Failure");
+        (TError, error_out_of_fuel_id, "OutOfFuel");
+        (* No Fuel::Zero on purpose *)
+        (* No Fuel::Succ on purpose *)
+      ]
 
 let assumed_llbc_functions () : (A.assumed_fun_id * string) list =
   match backend () with
-  | FStar | Coq | HOL4 ->
+  | FStar | Coq | HOL4 | IsabelleHOL ->
       [
         (ArrayIndexShared, "array_index_usize");
         (ArrayIndexMut, "array_index_mut_usize");
@@ -1175,6 +1212,9 @@ let assumed_pure_functions () : (pure_assumed_fun_id * string) list =
   | HOL4 ->
       (* We don't provide [FuelDecrease] and [FuelEqZero] on purpose *)
       [ (Return, "return"); (Fail, "fail"); (Assert, "massert") ]
+  | IsabelleHOL ->
+      (* We don't provide [FuelDecrease] and [FuelEqZero] on purpose *)
+      [ (Return, "return"); (Fail, "fail"); (Assert, "massert") ]
 
 let names_map_init () : names_map_init =
   {
@@ -1310,6 +1350,15 @@ let type_decl_kind_to_qualif (span : Meta.span) (kind : decl_kind)
       | Assumed -> Some "axiom"
       | Declared -> Some "axiom")
   | HOL4 -> None
+  | IsabelleHOL -> (
+      match kind with
+      | SingleNonRec -> Some "datatype"
+      | SingleRec -> Some "datatype"
+      | MutRecFirst -> Some "datatype"
+      | MutRecInner -> Some "and"
+      | MutRecLast -> Some "and"
+      | Assumed -> Some "axiomatization"
+      | Declared -> Some "aximoatization")
 
 (** Compute the qualified for a function definition/declaration.
 
@@ -1347,6 +1396,15 @@ let fun_decl_kind_to_qualif (kind : decl_kind) : string option =
       | Assumed -> Some "axiom"
       | Declared -> Some "axiom")
   | HOL4 -> None
+  | IsabelleHOL -> (
+      match kind with
+      | SingleNonRec -> Some "fun"
+      | SingleRec -> Some "fun"
+      | MutRecFirst -> Some "fun"
+      | MutRecInner -> Some "and"
+      | MutRecLast -> Some "and"
+      | Assumed -> Some "axiomatization"
+      | Declared -> Some "axiomatization")
 
 (** The type of types.
 
@@ -1356,7 +1414,7 @@ let type_keyword (span : Meta.span) =
   match backend () with
   | FStar -> "Type0"
   | Coq | Lean -> "Type"
-  | HOL4 -> craise __FILE__ __LINE__ span "Unexpected"
+  | HOL4 | IsabelleHOL -> craise __FILE__ __LINE__ span "Unexpected"
 
 (** Helper *)
 let name_last_elem_as_ident (span : Meta.span) (n : llbc_name) : string =
@@ -1410,7 +1468,7 @@ let ctx_compute_type_name (item_meta : Types.item_meta) (ctx : extraction_ctx)
   match backend () with
   | FStar -> StringUtils.lowercase_first_letter (name ^ "_t")
   | Coq | HOL4 -> name ^ "_t"
-  | Lean -> name
+  | Lean | IsabelleHOL -> name
 
 (** Inputs:
     - type name
@@ -1447,7 +1505,7 @@ let ctx_compute_field_name (def : type_decl) (field_meta : Meta.attr_info)
       ^ "_" ^ field_name_s
   in
   match backend () with
-  | Lean | HOL4 -> name
+  | Lean | HOL4 | IsabelleHOL -> name
   | Coq | FStar -> StringUtils.lowercase_first_letter name
 
 (** Inputs:
@@ -1461,7 +1519,7 @@ let ctx_compute_variant_name (ctx : extraction_ctx) (def : type_decl)
     Option.value variant.attr_info.rename ~default:variant.variant_name
   in
   match backend () with
-  | FStar | Coq | HOL4 ->
+  | FStar | Coq | HOL4 | IsabelleHOL ->
       let variant = to_camel_case variant in
       (* Prefix the name of the variant with the name of the type, if necessary
          (some backends don't support collision of variant names) *)
@@ -1494,14 +1552,14 @@ let ctx_compute_fun_name_no_suffix (span : Meta.span) (ctx : extraction_ctx)
   (* TODO: don't convert to snake case for Coq, HOL4, F* *)
   let fname = flatten_name fname in
   match backend () with
-  | FStar | Coq | HOL4 -> StringUtils.lowercase_first_letter fname
+  | FStar | Coq | HOL4 | IsabelleHOL -> StringUtils.lowercase_first_letter fname
   | Lean -> fname
 
 (** Provided a basename, compute the name of a global declaration. *)
 let ctx_compute_global_name (span : Meta.span) (ctx : extraction_ctx)
     (name : llbc_name) : string =
   match Config.backend () with
-  | Coq | FStar | HOL4 ->
+  | Coq | FStar | HOL4 | IsabelleHOL ->
       let parts =
         List.map to_snake_case (ctx_compute_simple_name span ctx name)
       in
@@ -1582,7 +1640,7 @@ let ctx_compute_trait_impl_name (ctx : extraction_ctx) (trait_decl : trait_decl)
   (* Additional modifications to make sure we comply with the backends restrictions *)
   match backend () with
   | FStar -> StringUtils.lowercase_first_letter name
-  | Coq | HOL4 | Lean -> name
+  | Coq | HOL4 | Lean | IsabelleHOL -> name
 
 let ctx_compute_trait_decl_constructor (ctx : extraction_ctx)
     (trait_decl : trait_decl) : string =
@@ -1659,7 +1717,7 @@ let ctx_compute_trait_parent_clause_name (ctx : extraction_ctx)
   let clause = clause ^ "Inst" in
   match backend () with
   | FStar -> StringUtils.lowercase_first_letter clause
-  | Coq | HOL4 | Lean -> clause
+  | Coq | HOL4 | Lean | IsabelleHOL -> clause
 
 let ctx_compute_trait_type_name (ctx : extraction_ctx) (trait_decl : trait_decl)
     (item : string) : string =
@@ -1676,7 +1734,7 @@ let ctx_compute_trait_type_name (ctx : extraction_ctx) (trait_decl : trait_decl)
      can't disambiguate fields coming from different ADTs if they have the same
      names), and thus don't need to add a prefix starting with a lowercase.
   *)
-  match backend () with FStar -> "t" ^ name | Coq | Lean | HOL4 -> name
+  match backend () with FStar -> "t" ^ name | Coq | Lean | HOL4 | IsabelleHOL -> name
 
 let ctx_compute_trait_const_name (ctx : extraction_ctx)
     (trait_decl : trait_decl) (item : string) : string =
@@ -1685,7 +1743,7 @@ let ctx_compute_trait_const_name (ctx : extraction_ctx)
     else ctx_compute_trait_decl_name ctx trait_decl ^ "_" ^ item
   in
   (* See [trait_type_name] *)
-  match backend () with FStar -> "c" ^ name | Coq | Lean | HOL4 -> name
+  match backend () with FStar -> "c" ^ name | Coq | Lean | HOL4 | IsabelleHOL -> name
 
 let ctx_compute_trait_method_name (ctx : extraction_ctx)
     (trait_decl : trait_decl) (item : string) : string =
@@ -1723,7 +1781,7 @@ let ctx_compute_termination_measure_name (span : Meta.span)
     match Config.backend () with
     | FStar -> "_decreases"
     | Lean -> "_terminates"
-    | Coq | HOL4 -> craise __FILE__ __LINE__ span "Unexpected"
+    | Coq | HOL4 | IsabelleHOL -> craise __FILE__ __LINE__ span "Unexpected"
   in
   (* Concatenate *)
   fname ^ lp_suffix ^ suffix
@@ -1751,7 +1809,7 @@ let ctx_compute_decreases_proof_name (span : Meta.span) (ctx : extraction_ctx)
   let suffix =
     match Config.backend () with
     | Lean -> "_decreases"
-    | FStar | Coq | HOL4 -> craise __FILE__ __LINE__ span "Unexpected"
+    | FStar | Coq | HOL4 | IsabelleHOL -> craise __FILE__ __LINE__ span "Unexpected"
   in
   (* Concatenate *)
   fname ^ lp_suffix ^ suffix
@@ -1792,7 +1850,7 @@ let ctx_compute_var_basename (span : Meta.span) (ctx : extraction_ctx)
       (* This should be a no-op *)
       match Config.backend () with
       | Lean -> basename
-      | FStar | Coq | HOL4 -> to_snake_case basename)
+      | FStar | Coq | HOL4 | IsabelleHOL -> to_snake_case basename)
   | None -> (
       (* No basename: we use the first letter of the type *)
       match ty with
@@ -1824,7 +1882,7 @@ let ctx_compute_var_basename (span : Meta.span) (ctx : extraction_ctx)
           (* TODO: use "t" also for F* *)
           match backend () with
           | FStar -> "x" (* lacking inspiration here... *)
-          | Coq | Lean | HOL4 -> "t" (* lacking inspiration here... *))
+          | Coq | Lean | HOL4 | IsabelleHOL -> "t" (* lacking inspiration here... *))
       | TLiteral lty -> (
           match lty with TBool -> "b" | TChar -> "c" | TInteger _ -> "i")
       | TArrow _ -> "f"
@@ -1839,7 +1897,7 @@ let ctx_compute_type_var_basename (_ctx : extraction_ctx) (basename : string) :
   | FStar ->
       (* This is *not* a no-op: this removes the capital letter *)
       to_snake_case basename
-  | HOL4 ->
+  | HOL4 | IsabelleHOL ->
       (* In HOL4, type variable names must start with "'" *)
       "'" ^ to_snake_case basename
   | Coq | Lean -> basename
@@ -1849,7 +1907,7 @@ let ctx_compute_const_generic_var_basename (_ctx : extraction_ctx)
     (basename : string) : string =
   (* Rust type variables are snake-case and start with a capital letter *)
   match backend () with
-  | FStar | HOL4 ->
+  | FStar | HOL4 | IsabelleHOL ->
       (* This is *not* a no-op: this removes the capital letter *)
       to_snake_case basename
   | Coq | Lean -> basename
@@ -1871,7 +1929,7 @@ let ctx_compute_trait_clause_basename (ctx : extraction_ctx)
   in
   let clause = clause ^ "Inst" in
   match backend () with
-  | FStar | Coq | HOL4 -> StringUtils.lowercase_first_letter clause
+  | FStar | Coq | HOL4 | IsabelleHOL -> StringUtils.lowercase_first_letter clause
   | Lean -> clause
 
 let trait_self_clause_basename = "self_clause"
diff --git a/compiler/ExtractBuiltin.ml b/compiler/ExtractBuiltin.ml
index 37b676bb..f0460035 100644
--- a/compiler/ExtractBuiltin.ml
+++ b/compiler/ExtractBuiltin.ml
@@ -44,7 +44,7 @@ let split_on_separator (s : string) : string list =
 
 let flatten_name (name : string list) : string =
   match backend () with
-  | FStar | Coq | HOL4 -> String.concat "_" name
+  | FStar | Coq | HOL4 | IsabelleHOL -> String.concat "_" name
   | Lean -> String.concat "." name
 
 (** Utility for Lean-only definitions **)
@@ -61,7 +61,7 @@ let () =
     is F*, Coq or HOL4, and a different value if the target is Lean.
  *)
 let backend_choice (fstar_coq_hol4 : 'a) (lean : 'a) : 'a =
-  match backend () with Coq | FStar | HOL4 -> fstar_coq_hol4 | Lean -> lean
+  match backend () with Coq | FStar | HOL4 | IsabelleHOL -> fstar_coq_hol4 | Lean -> lean
 
 let builtin_globals : (string * string) list =
   [
@@ -135,10 +135,10 @@ type type_variant_kind =
 
 let mk_struct_constructor (type_name : string) : string =
   let prefix =
-    match backend () with FStar -> "Mk" | Coq | HOL4 -> "mk" | Lean -> ""
+    match backend () with FStar -> "Mk" | Coq | HOL4 | IsabelleHOL -> "mk" | Lean -> ""
   in
   let suffix =
-    match backend () with FStar | Coq | HOL4 -> "" | Lean -> ".mk"
+    match backend () with FStar | Coq | HOL4 | IsabelleHOL -> "" | Lean -> ".mk"
   in
   prefix ^ type_name ^ suffix
 
@@ -168,7 +168,7 @@ let builtin_types () : builtin_type_info list =
                 ( rname,
                   match backend () with
                   | FStar | Lean -> name
-                  | Coq | HOL4 -> extract_name ^ "_" ^ name ))
+                  | Coq | HOL4 | IsabelleHOL -> extract_name ^ "_" ^ name ))
               fields
           in
           let constructor = mk_struct_constructor extract_name in
@@ -201,7 +201,7 @@ let builtin_types () : builtin_type_info list =
       extract_name =
         (match backend () with
         | Lean -> "Option"
-        | Coq | FStar | HOL4 -> "option");
+        | Coq | FStar | HOL4 | IsabelleHOL -> "option");
       keep_params = None;
       body_info =
         Some
@@ -211,7 +211,7 @@ let builtin_types () : builtin_type_info list =
                  rust_variant_name = "None";
                  extract_variant_name =
                    (match backend () with
-                   | FStar | Coq -> "None"
+                   | FStar | Coq | IsabelleHOL -> "None"
                    | Lean -> "none"
                    | HOL4 -> "NONE");
                  fields = None;
@@ -220,7 +220,7 @@ let builtin_types () : builtin_type_info list =
                  rust_variant_name = "Some";
                  extract_variant_name =
                    (match backend () with
-                   | FStar | Coq -> "Some"
+                   | FStar | Coq | IsabelleHOL -> "Some"
                    | Lean -> "some"
                    | HOL4 -> "SOME");
                  fields = None;
@@ -574,7 +574,7 @@ let builtin_trait_decls_info () =
         in
         let type_name =
           match backend () with
-          | FStar | Coq | HOL4 -> StringUtils.lowercase_first_letter type_name
+          | FStar | Coq | HOL4 | IsabelleHOL -> StringUtils.lowercase_first_letter type_name
           | Lean -> type_name
         in
         let clauses = [] in
diff --git a/compiler/ExtractTypes.ml b/compiler/ExtractTypes.ml
index 78382179..0162310a 100644
--- a/compiler/ExtractTypes.ml
+++ b/compiler/ExtractTypes.ml
@@ -23,7 +23,7 @@ let extract_literal (span : Meta.span) (fmt : F.formatter) (is_pattern : bool)
   | VScalar sv -> (
       match backend () with
       | FStar -> F.pp_print_string fmt (Z.to_string sv.value)
-      | Coq | HOL4 | Lean ->
+      | Coq | HOL4 | Lean | IsabelleHOL ->
           let print_brackets = inside && backend () = HOL4 in
           if print_brackets then F.pp_print_string fmt "(";
           (match backend () with
@@ -54,6 +54,7 @@ let extract_literal (span : Meta.span) (fmt : F.formatter) (is_pattern : bool)
         match backend () with
         | HOL4 -> if b then "T" else "F"
         | Coq | FStar | Lean -> if b then "true" else "false"
+        | IsabelleHOL -> if b then "True" else "False"
       in
       F.pp_print_string fmt b
   | VChar c -> (
@@ -62,6 +63,7 @@ let extract_literal (span : Meta.span) (fmt : F.formatter) (is_pattern : bool)
           (* [#"a"] is a notation for [CHR 97] (97 is the ASCII code for 'a') *)
           F.pp_print_string fmt ("#\"" ^ String.make 1 c ^ "\"")
       | FStar | Lean -> F.pp_print_string fmt ("'" ^ String.make 1 c ^ "'")
+      | IsabelleHOL -> F.pp_print_string fmt ("CHR ''" ^ String.make 1 c ^ "''")
       | Coq ->
           if inside then F.pp_print_string fmt "(";
           F.pp_print_string fmt "char_of_byte";
@@ -105,7 +107,7 @@ let extract_unop (span : Meta.span) (extract_expr : bool -> texpression -> unit)
       (* HOL4 has a special treatment: because it doesn't support dependent
          types, we don't have a specific operator for the cast *)
       match backend () with
-      | HOL4 ->
+      | HOL4 | IsabelleHOL ->
           (* Casting, say, an u32 to an i32 would be done as follows:
              {[
                mk_i32 (u32_to_int x)
@@ -135,7 +137,7 @@ let extract_unop (span : Meta.span) (extract_expr : bool -> texpression -> unit)
              | TInteger src, TInteger tgt ->
                  let cast_str =
                    match backend () with
-                   | Coq | FStar -> "scalar_cast"
+                   | Coq | FStar | IsabelleHOL -> "scalar_cast"
                    | Lean -> "Scalar.cast"
                    | HOL4 -> craise __FILE__ __LINE__ span "Unreachable"
                  in
@@ -148,7 +150,7 @@ let extract_unop (span : Meta.span) (extract_expr : bool -> texpression -> unit)
              | TBool, TInteger tgt ->
                  let cast_str =
                    match backend () with
-                   | Coq | FStar -> "scalar_cast_bool"
+                   | Coq | FStar | IsabelleHOL -> "scalar_cast_bool"
                    | Lean -> "Scalar.cast_bool"
                    | HOL4 -> craise __FILE__ __LINE__ span "Unreachable"
                  in
@@ -205,6 +207,7 @@ let extract_binop (span : Meta.span)
   (* Some binary operations have a special notation depending on the backend *)
   (match (backend (), binop) with
   | HOL4, (Eq | Ne)
+  | IsabelleHOL, (Eq | Ne)
   | (FStar | Coq | Lean), (Eq | Lt | Le | Ne | Ge | Gt)
   | Lean, (Div | Rem | Add | Sub | Mul | Shl | Shr | BitXor | BitOr | BitAnd) ->
       let binop =
@@ -231,7 +234,7 @@ let extract_binop (span : Meta.span)
       in
       let binop =
         match backend () with
-        | FStar | Lean | HOL4 -> binop
+        | FStar | Lean | HOL4 | IsabelleHOL -> binop
         | Coq -> "s" ^ binop
       in
       extract_expr false arg0;
@@ -283,7 +286,7 @@ let is_empty_record_type_decl_group (dg : Pure.type_decl list) : bool =
 let start_fun_decl_group (ctx : extraction_ctx) (fmt : F.formatter)
     (is_rec : bool) (dg : Pure.fun_decl list) =
   match backend () with
-  | FStar | Coq | Lean -> ()
+  | FStar | Coq | Lean | IsabelleHOL -> ()
   | HOL4 ->
       (* In HOL4, opaque functions have a special treatment *)
       if is_single_opaque_fun_decl_group dg then ()
@@ -313,7 +316,7 @@ let start_fun_decl_group (ctx : extraction_ctx) (fmt : F.formatter)
 let end_fun_decl_group (fmt : F.formatter) (is_rec : bool)
     (dg : Pure.fun_decl list) =
   match backend () with
-  | FStar -> ()
+  | FStar | IsabelleHOL -> ()
   | Coq ->
       (* For aesthetic reasons, we print the Coq end group delimiter directly
          in {!extract_fun_decl}. *)
@@ -344,7 +347,7 @@ let end_fun_decl_group (fmt : F.formatter) (is_rec : bool)
 let start_type_decl_group (ctx : extraction_ctx) (fmt : F.formatter)
     (is_rec : bool) (dg : Pure.type_decl list) =
   match backend () with
-  | FStar | Coq -> ()
+  | FStar | Coq | IsabelleHOL -> ()
   | Lean ->
       if is_rec && List.length dg > 1 then (
         F.pp_print_space fmt ();
@@ -371,7 +374,7 @@ let start_type_decl_group (ctx : extraction_ctx) (fmt : F.formatter)
 let end_type_decl_group (fmt : F.formatter) (is_rec : bool)
     (dg : Pure.type_decl list) =
   match backend () with
-  | FStar -> ()
+  | FStar | IsabelleHOL -> ()
   | Coq ->
       (* For aesthetic reasons, we print the Coq end group delimiter directly
          in {!extract_fun_decl}. *)
@@ -402,12 +405,14 @@ let end_type_decl_group (fmt : F.formatter) (is_rec : bool)
         F.pp_print_break fmt 0 0)
 
 let unit_name () =
-  match backend () with Lean -> "Unit" | Coq | FStar | HOL4 -> "unit"
+  match backend () with Lean -> "Unit" | Coq | FStar | HOL4 | IsabelleHOL -> "unit"
 
 (** Small helper *)
 let extract_arrow (fmt : F.formatter) () : unit =
-  if Config.backend () = Lean then F.pp_print_string fmt "→"
-  else F.pp_print_string fmt "->"
+  match Config.backend() with
+  | Lean -> F.pp_print_string fmt "→"
+  | IsabelleHOL -> F.pp_print_string fmt "\\<Rightarrow>"
+  | _ -> F.pp_print_string fmt "->"
 
 let extract_const_generic (span : Meta.span) (ctx : extraction_ctx)
     (fmt : F.formatter) (inside : bool) (cg : const_generic) : unit =
@@ -452,7 +457,7 @@ let extract_ty_errors (fmt : F.formatter) : unit =
   match Config.backend () with
   | FStar | Coq -> F.pp_print_string fmt "admit"
   | Lean -> F.pp_print_string fmt "sorry"
-  | HOL4 -> F.pp_print_string fmt "(* ERROR: could not generate the code *)"
+  | HOL4 | IsabelleHOL -> F.pp_print_string fmt "(* ERROR: could not generate the code *)"
 
 let rec extract_ty (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter)
     (no_params_tys : TypeDeclId.Set.t) (inside : bool) (ty : ty) : unit =
@@ -473,7 +478,7 @@ let rec extract_ty (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter)
                 let product =
                   match backend () with
                   | FStar -> "&"
-                  | Coq -> "*"
+                  | Coq | IsabelleHOL -> "*"
                   | Lean -> "×"
                   | HOL4 -> "#"
                 in
@@ -517,7 +522,7 @@ let rec extract_ty (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter)
               in
               extract_generic_args span ctx fmt no_params_tys generics;
               if print_paren then F.pp_print_string fmt ")"
-          | HOL4 ->
+          | HOL4 | IsabelleHOL ->
               let { types; const_generics; trait_refs } = generics in
               (* Const generics are not supported in HOL4 *)
               cassert __FILE__ __LINE__ (const_generics = []) span
@@ -869,15 +874,16 @@ let extract_type_decl_register_names (ctx : extraction_ctx) (def : type_decl) :
 let extract_type_decl_variant (span : Meta.span) (ctx : extraction_ctx)
     (fmt : F.formatter) (type_decl_group : TypeDeclId.Set.t)
     (type_name : string) (type_params : string list) (cg_params : string list)
-    (cons_name : string) (fields : field list) : unit =
+    (cons_name : string) (fields : field list) (index : int): unit =
   F.pp_print_space fmt ();
   (* variant box *)
   F.pp_open_hvbox fmt ctx.indent_incr;
   (* [| Cons :]
    * Note that we really don't want any break above so we print everything
    * at once. *)
-  let opt_colon = if backend () <> HOL4 then " :" else "" in
-  F.pp_print_string fmt ("| " ^ cons_name ^ opt_colon);
+  let opt_colon = if backend () <> HOL4 && backend () <> IsabelleHOL then " :" else "" in
+  let colon = if backend () <> IsabelleHOL || index <> 0 then "| " else "" in
+  F.pp_print_string fmt (colon ^ cons_name ^ opt_colon);
   let print_field (fid : FieldId.id) (f : field) (ctx : extraction_ctx) :
       extraction_ctx =
     F.pp_print_space fmt ();
@@ -901,7 +907,7 @@ let extract_type_decl_variant (span : Meta.span) (ctx : extraction_ctx)
               F.pp_print_string fmt (field_name ^ " :");
               F.pp_print_space fmt ();
               ctx)
-      | Coq | Lean | HOL4 -> ctx
+      | Coq | Lean | HOL4 | IsabelleHOL -> ctx
     in
     (* Print the field type *)
     let inside = backend () = HOL4 in
@@ -923,7 +929,7 @@ let extract_type_decl_variant (span : Meta.span) (ctx : extraction_ctx)
   (* Sanity check: HOL4 doesn't support const generics *)
   sanity_check __FILE__ __LINE__ (cg_params = [] || backend () <> HOL4) span;
   (* Print the final type *)
-  if backend () <> HOL4 then (
+  if backend () <> HOL4 && backend () <> IsabelleHOL then (
     F.pp_print_space fmt ();
     F.pp_open_hovbox fmt 0;
     F.pp_print_string fmt type_name;
@@ -973,13 +979,13 @@ let extract_type_decl_enum_body (ctx : extraction_ctx) (fmt : F.formatter)
 
      Note that we already printed: [type s =]
   *)
-  let print_variant _variant_id (v : variant) =
+  let print_variant variant_id (v : variant) =
     (* We don't lookup the name, because it may have a prefix for the type
        id (in the case of Lean) *)
     let cons_name = ctx_compute_variant_name ctx def v in
     let fields = v.fields in
     extract_type_decl_variant def.item_meta.span ctx fmt type_decl_group
-      def_name type_params cg_params cons_name fields
+      def_name type_params cg_params cons_name fields (VariantId.to_int variant_id)
   in
   (* Print the variants *)
   let variants = VariantId.mapi (fun vid v -> (vid, v)) variants in
@@ -993,7 +999,7 @@ let extract_type_decl_tuple_struct_body (span : Meta.span)
     F.pp_print_space fmt ();
     F.pp_print_string fmt (unit_name ()))
   else
-    let sep = match backend () with Coq | FStar | HOL4 -> "*" | Lean -> "×" in
+    let sep = match backend () with Coq | FStar | HOL4 | IsabelleHOL -> "*" | Lean -> "×" in
     Collections.List.iter_link
       (fun () ->
         F.pp_print_space fmt ();
@@ -1072,22 +1078,26 @@ let extract_type_decl_struct_body (ctx : extraction_ctx) (fmt : F.formatter)
          (instead of a record). We start with the "normal" case: we extract it
          as a record. *)
     else if (not is_rec) || (backend () <> Coq && backend () <> Lean) then (
-      if backend () <> Lean then F.pp_print_space fmt ();
-      (* If Coq: print the constructor name *)
+      if backend () <> Lean then (
+        if backend () = IsabelleHOL then
+          F.pp_print_string fmt " "
+        else F.pp_print_space fmt ());
+      (* If Coq or Isabelle: print the constructor name *)
       (* TODO: remove superfluous test not is_rec below *)
-      if backend () = Coq && not is_rec then (
+      if (backend () = Coq && not is_rec) || backend () = IsabelleHOL then (
         F.pp_print_string fmt
           (ctx_get_struct def.item_meta.span (TAdtId def.def_id) ctx);
-        F.pp_print_string fmt " ");
+        if backend () = Coq then
+          F.pp_print_string fmt " ");
       (match backend () with
-      | Lean -> ()
+      | Lean | IsabelleHOL -> ()
       | FStar | Coq -> F.pp_print_string fmt "{"
       | HOL4 -> F.pp_print_string fmt "<|");
       F.pp_print_break fmt 1 ctx.indent_incr;
       (* The body itself *)
       (* Open a box for the body *)
       (match backend () with
-      | Coq | FStar | HOL4 -> F.pp_open_hvbox fmt 0
+      | Coq | FStar | HOL4 | IsabelleHOL -> F.pp_open_hvbox fmt 0
       | Lean -> F.pp_open_vbox fmt 0);
       (* Print the fields *)
       let print_field (field_id : FieldId.id) (f : field) : unit =
@@ -1096,12 +1106,19 @@ let extract_type_decl_struct_body (ctx : extraction_ctx) (fmt : F.formatter)
         in
         (* Open a box for the field *)
         F.pp_open_box fmt ctx.indent_incr;
+        if backend () = IsabelleHOL then
+          F.pp_print_string fmt "(";
         F.pp_print_string fmt field_name;
-        F.pp_print_space fmt ();
+        if backend () <> IsabelleHOL then
+          F.pp_print_space fmt ();
         F.pp_print_string fmt ":";
         F.pp_print_space fmt ();
+        if backend () = IsabelleHOL then
+          F.pp_print_string fmt "\"";
         extract_ty def.item_meta.span ctx fmt type_decl_group false f.field_ty;
-        if backend () <> Lean then F.pp_print_string fmt ";";
+        if backend () <> Lean && backend () <> IsabelleHOL then F.pp_print_string fmt ";";
+        if backend () = IsabelleHOL then
+          F.pp_print_string fmt "\")";
         (* Close the box for the field *)
         F.pp_close_box fmt ()
       in
@@ -1112,7 +1129,7 @@ let extract_type_decl_struct_body (ctx : extraction_ctx) (fmt : F.formatter)
       (* Close the box for the body *)
       F.pp_close_box fmt ();
       match backend () with
-      | Lean -> ()
+      | Lean | IsabelleHOL -> ()
       | FStar | Coq ->
           F.pp_print_space fmt ();
           F.pp_print_string fmt "}"
@@ -1136,7 +1153,7 @@ let extract_type_decl_struct_body (ctx : extraction_ctx) (fmt : F.formatter)
       in
       let def_name = ctx_get_local_type def.item_meta.span def.def_id ctx in
       extract_type_decl_variant def.item_meta.span ctx fmt type_decl_group
-        def_name type_params cg_params cons_name fields)
+        def_name type_params cg_params cons_name fields 0)
   in
   ()
 
@@ -1146,6 +1163,7 @@ let extract_comment (fmt : F.formatter) (sl : string list) : unit =
   let ld, space, rd =
     match backend () with
     | Coq | FStar | HOL4 -> ("(** ", 4, " *)")
+    | IsabelleHOL -> ("(*", 3, "*)")
     | Lean -> ("/- ", 3, " -/")
   in
   F.pp_open_vbox fmt space;
@@ -1263,7 +1281,7 @@ let extract_generic_params (span : Meta.span) (ctx : extraction_ctx)
         (const_generics : const_generic_var list)
         (trait_clauses : trait_clause list) : unit =
       (* Note that in HOL4 we don't print the type parameters. *)
-      if backend () <> HOL4 then (
+      if backend () <> HOL4 && backend () <> IsabelleHOL then (
         (* Print the type parameters *)
         if type_params <> [] then (
           insert_req_space ();
@@ -1437,7 +1455,7 @@ let extract_type_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
    * one line. Note however that in the case of Lean line breaks are important
    * for parsing: we thus use a hovbox. *)
   (match backend () with
-  | Coq | FStar | HOL4 -> F.pp_open_hvbox fmt 0
+  | Coq | FStar | HOL4 | IsabelleHOL -> F.pp_open_hvbox fmt 0
   | Lean ->
       if is_tuple_struct then F.pp_open_hvbox fmt 0 else F.pp_open_vbox fmt 0);
   (* Open a box for "type TYPE_NAME (TYPE_PARAMS CONST_GEN_PARAMS) =" *)
@@ -1479,7 +1497,7 @@ let extract_type_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
       | Lean ->
           if type_kind = Some Struct && kind = SingleNonRec then "where"
           else ":="
-      | HOL4 -> "="
+      | HOL4 | IsabelleHOL -> "="
     in
     F.pp_print_string fmt eq)
   else (
@@ -1519,6 +1537,11 @@ let extract_type_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
   F.pp_close_box fmt ();
   (* Add breaks to insert new lines between definitions *)
   if backend () <> HOL4 || decl_is_not_last_from_group kind then
+    F.pp_print_break fmt 0 0;
+
+  (* magic invocation to get field extractor functions & struct updates *)
+  if backend () = IsabelleHOL && type_kind = Some Struct then
+    F.pp_print_string fmt ("local_setup \\<open>Datatype_Records.mk_update_defs \\<^type_name>\\<open>"^def_name^"\\<close>\\<close>");
     F.pp_print_break fmt 0 0
 
 (** Extract an opaque type declaration to HOL4.
@@ -1558,6 +1581,7 @@ let extract_type_decl_hol4_opaque (ctx : extraction_ctx) (fmt : F.formatter)
     Remark (SH): having to treat this specific case separately is very annoying,
     but I could not find a better way.
  *)
+(* TODO: same must be done for Isabelle *)
 let extract_type_decl_hol4_empty_record (ctx : extraction_ctx)
     (fmt : F.formatter) (def : type_decl) : unit =
   (* Retrieve the definition name *)
@@ -1595,7 +1619,7 @@ let extract_type_decl (ctx : extraction_ctx) (fmt : F.formatter)
     match backend () with
     | FStar | Coq | Lean ->
         extract_type_decl_gen ctx fmt type_decl_group kind def extract_body
-    | HOL4 -> extract_type_decl_hol4_opaque ctx fmt def
+    | HOL4 | IsabelleHOL -> extract_type_decl_hol4_opaque ctx fmt def
 
 (** Generate a [Argument] instruction in Coq to allow omitting implicit
     arguments for variants, fields, etc..
@@ -1894,7 +1918,7 @@ let extract_type_decl_record_field_projectors (ctx : extraction_ctx)
 let extract_type_decl_extra_info (ctx : extraction_ctx) (fmt : F.formatter)
     (kind : decl_kind) (decl : type_decl) : unit =
   match backend () with
-  | FStar | HOL4 -> ()
+  | FStar | HOL4 | IsabelleHOL -> ()
   | Lean | Coq ->
       if
         not
@@ -1924,6 +1948,7 @@ let extract_state_type (fmt : F.formatter) (ctx : extraction_ctx)
       match backend () with
       | Coq -> "Axiom"
       | Lean -> "axiom"
+      | IsabelleHOL -> "axiomatization"
       | FStar | HOL4 -> raise (Failure "Unexpected")
     in
     F.pp_print_string fmt axiom;
@@ -1953,7 +1978,7 @@ let extract_state_type (fmt : F.formatter) (ctx : extraction_ctx)
           F.pp_print_string fmt "Type0"
       | HOL4 ->
           F.pp_print_string fmt ("val _ = new_type (\"" ^ state_name ^ "\", 0)")
-      | Coq | Lean -> print_axiom ())
+      | Coq | Lean | IsabelleHOL -> print_axiom ())
   | Declared -> (
       match backend () with
       | FStar ->
@@ -1966,7 +1991,7 @@ let extract_state_type (fmt : F.formatter) (ctx : extraction_ctx)
           F.pp_print_string fmt "Type0"
       | HOL4 ->
           F.pp_print_string fmt ("val _ = new_type (\"" ^ state_name ^ "\", 0)")
-      | Coq | Lean -> print_axiom ()));
+      | Coq | Lean | IsabelleHOL -> print_axiom ()));
   (* Close the box for the definition *)
   F.pp_close_box fmt ();
   (* Add breaks to insert new lines between definitions *)
diff --git a/compiler/Main.ml b/compiler/Main.ml
index d78b9081..ff6a4d67 100644
--- a/compiler/Main.ml
+++ b/compiler/Main.ml
@@ -253,6 +253,12 @@ let () =
             (* We don't support fuel for the HOL4 backend *)
             if !use_fuel then (
               log#error "The HOL4 backend doesn't support the -use-fuel option";
+              fail ())
+        | IsabelleHOL ->
+            record_fields_short_names := true;
+            (* We don't support fuel for the IsabelleHOL backend *)
+            if !use_fuel then (
+              log#error "The IsabelleHOL backend doesn't support the -use-fuel option";
               fail ()))
   in
 
diff --git a/compiler/PureUtils.ml b/compiler/PureUtils.ml
index 9673f542..a2ba5dbc 100644
--- a/compiler/PureUtils.ml
+++ b/compiler/PureUtils.ml
@@ -243,7 +243,7 @@ let rec let_group_requires_parentheses (span : Meta.span) (e : texpression) :
 let texpression_requires_parentheses span e =
   match Config.backend () with
   | FStar | Lean -> false
-  | Coq | HOL4 -> let_group_requires_parentheses span e
+  | Coq | HOL4 | IsabelleHOL -> let_group_requires_parentheses span e
 
 let is_var (e : texpression) : bool =
   match e.e with Var _ -> true | _ -> false
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index e829ed30..3f858124 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -3754,7 +3754,7 @@ let wrap_in_match_fuel (span : Meta.span) (fuel0 : VarId.id) (fuel : VarId.id)
       let match_ty = body.ty in
       let match_e = Switch (fuel0, Match [ fail_branch; success_branch ]) in
       { e = match_e; ty = match_ty }
-  | Lean | HOL4 ->
+  | Lean | HOL4 | IsabelleHOL ->
       (* We should have checked the command line arguments before *)
       raise (Failure "Unexpected")
 
diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index 672fb22f..afd3420e 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -692,6 +692,9 @@ let export_functions_group (fmt : Format.formatter) (config : gen_config)
               | HOL4 ->
                   raise
                     (Failure "HOL4 doesn't have decreases/termination clauses")
+              | IsabelleHOL ->
+                  raise
+                    (Failure "HOL4 doesn't have decreases/termination clauses")
           in
           extract_decrease f.f;
           List.iter extract_decrease f.loops)
@@ -886,7 +889,7 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (fi : extract_file_info)
   | Lean ->
       Printf.fprintf out "-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS\n";
       Printf.fprintf out "-- [%s]%s\n" fi.rust_module_name fi.custom_msg
-  | Coq | FStar | HOL4 ->
+  | Coq | FStar | HOL4 | IsabelleHOL ->
       Printf.fprintf out
         "(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)\n";
       Printf.fprintf out "(** [%s]%s *)\n" fi.rust_module_name fi.custom_msg);
@@ -968,7 +971,23 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (fi : extract_file_info)
         Printf.fprintf out "open %s\n\n" imports
       else Printf.fprintf out "\n";
       (* Initialize the theory *)
-      Printf.fprintf out "val _ = new_theory \"%s\"\n\n" fi.module_name);
+      Printf.fprintf out "val _ = new_theory \"%s\"\n\n" fi.module_name
+  | IsabelleHOL ->
+      Printf.fprintf out "theory \"%s\" imports\n" fi.module_name;
+      (* Add the custom imports and includes *)
+      let imports =
+        "Aeneas.Primitives"
+        :: "HOL-Library.Datatype_Records"
+        :: fi.custom_imports @ fi.custom_includes in
+      (* The imports are a list of module names: we need to add a "Theory" suffix *)
+      let imports = List.map (fun s -> "\"" ^ s ^ "\"") imports in
+      if imports <> [] then
+        let imports = String.concat "\n  " imports in
+        Printf.fprintf out "  %s\n" imports
+      else Printf.fprintf out "\n";
+      Printf.fprintf out "begin\n\n"
+      (* Initialize the theory *)
+  );
   (* From now onwards, we use the formatter *)
   (* Set the margin *)
   Format.pp_set_margin fmt 80;
@@ -988,7 +1007,8 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (fi : extract_file_info)
   | FStar -> ()
   | Lean -> if fi.in_namespace then Printf.fprintf out "end %s\n" fi.namespace
   | HOL4 -> Printf.fprintf out "val _ = export_theory ()\n"
-  | Coq -> Printf.fprintf out "End %s.\n" fi.module_name);
+  | Coq -> Printf.fprintf out "End %s.\n" fi.module_name
+  | IsabelleHOL -> Printf.fprintf out "end");
 
   (* Some logging *)
   if !Errors.error_list <> [] then
@@ -1148,7 +1168,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) :
         (* We use the raw crate name for the namespaces *)
         let namespace =
           match Config.backend () with
-          | FStar | Coq | HOL4 -> crate.name
+          | FStar | Coq | HOL4 | IsabelleHOL -> crate.name
           | Lean -> crate.name
         in
         (* Concatenate *)
@@ -1189,6 +1209,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) :
       | Coq -> Some ("/backends/coq/Primitives.v", "Primitives.v")
       | Lean -> None
       | HOL4 -> None
+      | IsabelleHOL -> None
     in
     match primitives_src_dest with
     | None -> ()
@@ -1223,6 +1244,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) :
     | Coq -> "_"
     | Lean -> "."
     | HOL4 -> "_"
+    | IsabelleHOL -> "."
   in
   let file_delimiter =
     if Config.backend () = Lean then "/" else module_delimiter
@@ -1234,6 +1256,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) :
     | Coq -> ".v"
     | Lean -> ".lean"
     | HOL4 -> "Script.sml"
+    | IsabelleHOL -> ".thy"
   in
   (* File extension for the opaque module *)
   let opaque_ext =
@@ -1242,6 +1265,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) :
     | Coq -> ".v"
     | Lean -> ".lean"
     | HOL4 -> "Script.sml"
+    | IsabelleHOL -> ".thy"
   in
 
   (* Extract one or several files, depending on the configuration *)
@@ -1284,7 +1308,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) :
            match Config.backend () with
            | FStar ->
                ("TypesExternal", "TypesExternal", ": external type declarations")
-           | HOL4 | Coq | Lean ->
+           | HOL4 | Coq | Lean | IsabelleHOL ->
                ( (* The name of the file we generate *)
                  "TypesExternal_Template",
                  (* The name of the file that will be imported by the Types
@@ -1339,6 +1363,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) :
        | Coq -> ".v"
        | Lean -> ".lean"
        | HOL4 -> "Script.sml"
+       | IsabelleHOL -> ".thy"
      in
      let types_filename =
        extract_filebasename ^ file_delimiter ^ "Types" ^ types_filename_ext
@@ -1410,7 +1435,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) :
                ( "FunsExternal",
                  "FunsExternal",
                  ": external function declarations" )
-           | HOL4 | Coq | Lean ->
+           | HOL4 | Coq | Lean | IsabelleHOL ->
                ( (* The name of the file we generate *)
                  "FunsExternal_Template",
                  (* The name of the file that will be imported by the Funs
@@ -1530,7 +1555,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) :
 
   (* Generate the build file *)
   match Config.backend () with
-  | Coq | FStar | HOL4 ->
+  | Coq | FStar | HOL4 | IsabelleHOL ->
       ()
       (* Nothing to do - TODO: we might want to generate the _CoqProject file for Coq.
          But then we can't modify it if we want to add more files for the proofs