diff --git a/flake.lock b/flake.lock
index 1e77e707..9531578c 100644
--- a/flake.lock
+++ b/flake.lock
@@ -309,16 +309,16 @@
     },
     "isabelle-nixpkgs": {
       "locked": {
-        "lastModified": 1656007306,
-        "narHash": "sha256-MsC44YZ6wuBwn5Bu8T+RVoQWlp2l5BR6hhmNoAAHIEw=",
+        "lastModified": 1682535835,
+        "narHash": "sha256-DrCcsZId29H+mr7yviOfCZeJOnJ51MIWLX3qSwwSpLI=",
         "owner": "NixOS",
         "repo": "nixpkgs",
-        "rev": "ccf8bdf72624521358be6bb7d9b524c4cbcf7aff",
+        "rev": "d12fa94d29856187b1c80db4edf4588df986d217",
         "type": "github"
       },
       "original": {
         "id": "nixpkgs",
-        "ref": "nixos-22.05",
+        "ref": "nixpkgs-unstable",
         "type": "indirect"
       }
     },
diff --git a/flake.nix b/flake.nix
index 9daa9f0a..0e2671b9 100644
--- a/flake.nix
+++ b/flake.nix
@@ -8,7 +8,7 @@
 
     nixpkgs.follows = "haskellNix/nixpkgs-unstable";
 
-    isabelle-nixpkgs.url = "nixpkgs/nixos-22.05";
+    isabelle-nixpkgs.url = "nixpkgs/nixpkgs-unstable";
 
     nixLsp.url = "github:oxalica/nil";
 
@@ -66,6 +66,7 @@
               (with scripts; [
                 build-marlowe-proofs
                 edit-marlowe-proofs
+                vscode-marlowe-proofs
                 build-marlowe-docs
               ]
               ) ++
diff --git a/isabelle/CodeExports/CodeExports.thy b/isabelle/CodeExports/CodeExports.thy
index 87647a62..39fe762a 100644
--- a/isabelle/CodeExports/CodeExports.thy
+++ b/isabelle/CodeExports/CodeExports.thy
@@ -39,7 +39,7 @@ code_printing
   \<comment> \<open>into Haskell string. Because this is a textual rewrite, we need to force the\<close>
   \<comment> \<open>generation of String.implode\<close>
   | constant "BS :: string \<Rightarrow> ByteString"
-      \<rightharpoonup> (Haskell) "Stringa.implode"
+      \<rightharpoonup> (Haskell) "Str.implode"
 
 
 text \<open>With a \<^bold>\<open>code\_identifier\<close> we hint what the name of the module should be.\<close>
diff --git a/isabelle/generated/Examples/Escrow.hs b/isabelle/generated/Examples/Escrow.hs
index 84d4925e..a73bad70 100644
--- a/isabelle/generated/Examples/Escrow.hs
+++ b/isabelle/generated/Examples/Escrow.hs
@@ -15,7 +15,7 @@ import Prelude ((==), (/=), (<), (<=), (>=), (>), (+), (-), (*), (/), (**),
   String, Bool(True, False), Maybe(Nothing, Just));
 import qualified Prelude;
 import qualified Semantics;
-import qualified Stringa;
+import qualified Str;
 import qualified SemanticsTypes;
 import qualified Arith;
 
@@ -28,12 +28,12 @@ data EscrowArgs_ext a =
 buyer :: SemanticsTypes.Party;
 buyer =
   SemanticsTypes.Role
-    (Stringa.implode
-      [Stringa.Char False True False False False False True False,
-        Stringa.Char True False True False True True True False,
-        Stringa.Char True False False True True True True False,
-        Stringa.Char True False True False False True True False,
-        Stringa.Char False True False False True True True False]);
+    (Str.implode
+      [Str.Char False True False False False False True False,
+        Str.Char True False True False True True True False,
+        Str.Char True False False True True True True False,
+        Str.Char True False True False False True True False,
+        Str.Char False True False False True True True False]);
 
 paymentDeadline :: forall a. EscrowArgs_ext a -> Arith.Int;
 paymentDeadline
@@ -56,13 +56,13 @@ price (EscrowArgs_ext price token buyerParty sellerParty mediatorParty
 seller :: SemanticsTypes.Party;
 seller =
   SemanticsTypes.Role
-    (Stringa.implode
-      [Stringa.Char True True False False True False True False,
-        Stringa.Char True False True False False True True False,
-        Stringa.Char False False True True False True True False,
-        Stringa.Char False False True True False True True False,
-        Stringa.Char True False True False False True True False,
-        Stringa.Char False True False False True True True False]);
+    (Str.implode
+      [Str.Char True True False False True False True False,
+        Str.Char True False True False False True True False,
+        Str.Char False False True True False True True False,
+        Str.Char False False True True False True True False,
+        Str.Char True False True False False True True False,
+        Str.Char False True False False True True True False]);
 
 complaintDeadline :: forall a. EscrowArgs_ext a -> Arith.Int;
 complaintDeadline
@@ -85,15 +85,15 @@ mediationDeadline
 mediator :: SemanticsTypes.Party;
 mediator =
   SemanticsTypes.Role
-    (Stringa.implode
-      [Stringa.Char True False True True False False True False,
-        Stringa.Char True False True False False True True False,
-        Stringa.Char False False True False False True True False,
-        Stringa.Char True False False True False True True False,
-        Stringa.Char True False False False False True True False,
-        Stringa.Char False False True False True True True False,
-        Stringa.Char True True True True False True True False,
-        Stringa.Char False True False False True True True False]);
+    (Str.implode
+      [Str.Char True False True True False False True False,
+        Str.Char True False True False False True True False,
+        Str.Char False False True False False True True False,
+        Str.Char True False False True False True True False,
+        Str.Char True False False False False True True False,
+        Str.Char False False True False True True True False,
+        Str.Char True True True True False True True False,
+        Str.Char False True False False True True True False]);
 
 mediation :: EscrowArgs_ext () -> SemanticsTypes.Contract;
 mediation args =
@@ -101,20 +101,20 @@ mediation args =
     [SemanticsTypes.Case
        (SemanticsTypes.Choice
          (SemanticsTypes.ChoiceId
-           (Stringa.implode
-             [Stringa.Char False False True False False False True False,
-               Stringa.Char True False False True False True True False,
-               Stringa.Char True True False False True True True False,
-               Stringa.Char True False True True False True True False,
-               Stringa.Char True False False True False True True False,
-               Stringa.Char True True False False True True True False,
-               Stringa.Char True True False False True True True False,
-               Stringa.Char False False False False False True False False,
-               Stringa.Char True True False False False True True False,
-               Stringa.Char False False True True False True True False,
-               Stringa.Char True False False False False True True False,
-               Stringa.Char True False False True False True True False,
-               Stringa.Char True False True True False True True False])
+           (Str.implode
+             [Str.Char False False True False False False True False,
+               Str.Char True False False True False True True False,
+               Str.Char True True False False True True True False,
+               Str.Char True False True True False True True False,
+               Str.Char True False False True False True True False,
+               Str.Char True True False False True True True False,
+               Str.Char True True False False True True True False,
+               Str.Char False False False False False True False False,
+               Str.Char True True False False False True True False,
+               Str.Char False False True True False True True False,
+               Str.Char True False False False False True True False,
+               Str.Char True False False True False True True False,
+               Str.Char True False True True False True True False])
            mediator)
          [SemanticsTypes.Bound Arith.zero_int Arith.zero_int])
        (SemanticsTypes.Pay buyer (SemanticsTypes.Account seller) (token args)
@@ -122,20 +122,20 @@ mediation args =
       SemanticsTypes.Case
         (SemanticsTypes.Choice
           (SemanticsTypes.ChoiceId
-            (Stringa.implode
-              [Stringa.Char True True False False False False True False,
-                Stringa.Char True True True True False True True False,
-                Stringa.Char False True True True False True True False,
-                Stringa.Char False True True False False True True False,
-                Stringa.Char True False False True False True True False,
-                Stringa.Char False True False False True True True False,
-                Stringa.Char True False True True False True True False,
-                Stringa.Char False False False False False True False False,
-                Stringa.Char True True False False False True True False,
-                Stringa.Char False False True True False True True False,
-                Stringa.Char True False False False False True True False,
-                Stringa.Char True False False True False True True False,
-                Stringa.Char True False True True False True True False])
+            (Str.implode
+              [Str.Char True True False False False False True False,
+                Str.Char True True True True False True True False,
+                Str.Char False True True True False True True False,
+                Str.Char False True True False False True True False,
+                Str.Char True False False True False True True False,
+                Str.Char False True False False True True True False,
+                Str.Char True False True True False True True False,
+                Str.Char False False False False False True False False,
+                Str.Char True True False False False True True False,
+                Str.Char False False True True False True True False,
+                Str.Char True False False False False True True False,
+                Str.Char True False False True False True True False,
+                Str.Char True False True True False True True False])
             mediator)
           [SemanticsTypes.Bound Arith.one_int Arith.one_int])
         SemanticsTypes.Close]
@@ -147,44 +147,44 @@ dispute args =
     [SemanticsTypes.Case
        (SemanticsTypes.Choice
          (SemanticsTypes.ChoiceId
-           (Stringa.implode
-             [Stringa.Char True True False False False False True False,
-               Stringa.Char True True True True False True True False,
-               Stringa.Char False True True True False True True False,
-               Stringa.Char False True True False False True True False,
-               Stringa.Char True False False True False True True False,
-               Stringa.Char False True False False True True True False,
-               Stringa.Char True False True True False True True False,
-               Stringa.Char False False False False False True False False,
-               Stringa.Char False False False False True True True False,
-               Stringa.Char False True False False True True True False,
-               Stringa.Char True True True True False True True False,
-               Stringa.Char False True False False False True True False,
-               Stringa.Char False False True True False True True False,
-               Stringa.Char True False True False False True True False,
-               Stringa.Char True False True True False True True False])
+           (Str.implode
+             [Str.Char True True False False False False True False,
+               Str.Char True True True True False True True False,
+               Str.Char False True True True False True True False,
+               Str.Char False True True False False True True False,
+               Str.Char True False False True False True True False,
+               Str.Char False True False False True True True False,
+               Str.Char True False True True False True True False,
+               Str.Char False False False False False True False False,
+               Str.Char False False False False True True True False,
+               Str.Char False True False False True True True False,
+               Str.Char True True True True False True True False,
+               Str.Char False True False False False True True False,
+               Str.Char False False True True False True True False,
+               Str.Char True False True False False True True False,
+               Str.Char True False True True False True True False])
            seller)
          [SemanticsTypes.Bound Arith.one_int Arith.one_int])
        SemanticsTypes.Close,
       SemanticsTypes.Case
         (SemanticsTypes.Choice
           (SemanticsTypes.ChoiceId
-            (Stringa.implode
-              [Stringa.Char False False True False False False True False,
-                Stringa.Char True False False True False True True False,
-                Stringa.Char True True False False True True True False,
-                Stringa.Char False False False False True True True False,
-                Stringa.Char True False True False True True True False,
-                Stringa.Char False False True False True True True False,
-                Stringa.Char True False True False False True True False,
-                Stringa.Char False False False False False True False False,
-                Stringa.Char False False False False True True True False,
-                Stringa.Char False True False False True True True False,
-                Stringa.Char True True True True False True True False,
-                Stringa.Char False True False False False True True False,
-                Stringa.Char False False True True False True True False,
-                Stringa.Char True False True False False True True False,
-                Stringa.Char True False True True False True True False])
+            (Str.implode
+              [Str.Char False False True False False False True False,
+                Str.Char True False False True False True True False,
+                Str.Char True True False False True True True False,
+                Str.Char False False False False True True True False,
+                Str.Char True False True False True True True False,
+                Str.Char False False True False True True True False,
+                Str.Char True False True False False True True False,
+                Str.Char False False False False False True False False,
+                Str.Char False False False False True True True False,
+                Str.Char False True False False True True True False,
+                Str.Char True True True True False True True False,
+                Str.Char False True False False False True True False,
+                Str.Char False False True True False True True False,
+                Str.Char True False True False False True True False,
+                Str.Char True False True True False True True False])
             seller)
           [SemanticsTypes.Bound Arith.zero_int Arith.zero_int])
         (mediation args)]
@@ -196,49 +196,49 @@ report args =
     [SemanticsTypes.Case
        (SemanticsTypes.Choice
          (SemanticsTypes.ChoiceId
-           (Stringa.implode
-             [Stringa.Char True False True False False False True False,
-               Stringa.Char False True True False True True True False,
-               Stringa.Char True False True False False True True False,
-               Stringa.Char False True False False True True True False,
-               Stringa.Char True False False True True True True False,
-               Stringa.Char False False True False True True True False,
-               Stringa.Char False False False True False True True False,
-               Stringa.Char True False False True False True True False,
-               Stringa.Char False True True True False True True False,
-               Stringa.Char True True True False False True True False,
-               Stringa.Char False False False False False True False False,
-               Stringa.Char True False False True False True True False,
-               Stringa.Char True True False False True True True False,
-               Stringa.Char False False False False False True False False,
-               Stringa.Char True False False False False True True False,
-               Stringa.Char False False True True False True True False,
-               Stringa.Char False True False False True True True False,
-               Stringa.Char True False False True False True True False,
-               Stringa.Char True True True False False True True False,
-               Stringa.Char False False False True False True True False,
-               Stringa.Char False False True False True True True False])
+           (Str.implode
+             [Str.Char True False True False False False True False,
+               Str.Char False True True False True True True False,
+               Str.Char True False True False False True True False,
+               Str.Char False True False False True True True False,
+               Str.Char True False False True True True True False,
+               Str.Char False False True False True True True False,
+               Str.Char False False False True False True True False,
+               Str.Char True False False True False True True False,
+               Str.Char False True True True False True True False,
+               Str.Char True True True False False True True False,
+               Str.Char False False False False False True False False,
+               Str.Char True False False True False True True False,
+               Str.Char True True False False True True True False,
+               Str.Char False False False False False True False False,
+               Str.Char True False False False False True True False,
+               Str.Char False False True True False True True False,
+               Str.Char False True False False True True True False,
+               Str.Char True False False True False True True False,
+               Str.Char True True True False False True True False,
+               Str.Char False False False True False True True False,
+               Str.Char False False True False True True True False])
            buyer)
          [SemanticsTypes.Bound Arith.zero_int Arith.zero_int])
        SemanticsTypes.Close,
       SemanticsTypes.Case
         (SemanticsTypes.Choice
           (SemanticsTypes.ChoiceId
-            (Stringa.implode
-              [Stringa.Char False True False False True False True False,
-                Stringa.Char True False True False False True True False,
-                Stringa.Char False False False False True True True False,
-                Stringa.Char True True True True False True True False,
-                Stringa.Char False True False False True True True False,
-                Stringa.Char False False True False True True True False,
-                Stringa.Char False False False False False True False False,
-                Stringa.Char False False False False True True True False,
-                Stringa.Char False True False False True True True False,
-                Stringa.Char True True True True False True True False,
-                Stringa.Char False True False False False True True False,
-                Stringa.Char False False True True False True True False,
-                Stringa.Char True False True False False True True False,
-                Stringa.Char True False True True False True True False])
+            (Str.implode
+              [Str.Char False True False False True False True False,
+                Str.Char True False True False False True True False,
+                Str.Char False False False False True True True False,
+                Str.Char True True True True False True True False,
+                Str.Char False True False False True True True False,
+                Str.Char False False True False True True True False,
+                Str.Char False False False False False True False False,
+                Str.Char False False False False True True True False,
+                Str.Char False True False False True True True False,
+                Str.Char True True True True False True True False,
+                Str.Char False True False False False True True False,
+                Str.Char False False True True False True True False,
+                Str.Char True False True False False True True False,
+                Str.Char True False True True False True True False])
             buyer)
           [SemanticsTypes.Bound Arith.one_int Arith.one_int])
         (SemanticsTypes.Pay seller (SemanticsTypes.Account buyer) (token args)
@@ -257,8 +257,8 @@ exampleArgs :: EscrowArgs_ext ();
 exampleArgs =
   EscrowArgs_ext
     (SemanticsTypes.Constant (Arith.Int_of_integer (10 :: Integer)))
-    (SemanticsTypes.Token (Stringa.implode []) (Stringa.implode [])) buyer
-    seller mediator (Arith.Int_of_integer (1664812800000 :: Integer))
+    (SemanticsTypes.Token (Str.implode []) (Str.implode [])) buyer seller
+    mediator (Arith.Int_of_integer (1664812800000 :: Integer))
     (Arith.Int_of_integer (1664816400000 :: Integer))
     (Arith.Int_of_integer (1664820420000 :: Integer))
     (Arith.Int_of_integer (1664824440000 :: Integer)) ();
@@ -302,21 +302,21 @@ confirmClaimTransactions =
         Arith.Int_of_integer (1664813100000 :: Integer))
       [SemanticsTypes.IChoice
          (SemanticsTypes.ChoiceId
-           (Stringa.implode
-             [Stringa.Char False True False False True False True False,
-               Stringa.Char True False True False False True True False,
-               Stringa.Char False False False False True True True False,
-               Stringa.Char True True True True False True True False,
-               Stringa.Char False True False False True True True False,
-               Stringa.Char False False True False True True True False,
-               Stringa.Char False False False False False True False False,
-               Stringa.Char False False False False True True True False,
-               Stringa.Char False True False False True True True False,
-               Stringa.Char True True True True False True True False,
-               Stringa.Char False True False False False True True False,
-               Stringa.Char False False True True False True True False,
-               Stringa.Char True False True False False True True False,
-               Stringa.Char True False True True False True True False])
+           (Str.implode
+             [Str.Char False True False False True False True False,
+               Str.Char True False True False False True True False,
+               Str.Char False False False False True True True False,
+               Str.Char True True True True False True True False,
+               Str.Char False True False False True True True False,
+               Str.Char False False True False True True True False,
+               Str.Char False False False False False True False False,
+               Str.Char False False False False True True True False,
+               Str.Char False True False False True True True False,
+               Str.Char True True True True False True True False,
+               Str.Char False True False False False True True False,
+               Str.Char False False True True False True True False,
+               Str.Char True False True False False True True False,
+               Str.Char True False True True False True True False])
            buyer)
          Arith.one_int]
       (),
@@ -325,22 +325,22 @@ confirmClaimTransactions =
         Arith.Int_of_integer (1664817400000 :: Integer))
       [SemanticsTypes.IChoice
          (SemanticsTypes.ChoiceId
-           (Stringa.implode
-             [Stringa.Char False False True False False False True False,
-               Stringa.Char True False False True False True True False,
-               Stringa.Char True True False False True True True False,
-               Stringa.Char False False False False True True True False,
-               Stringa.Char True False True False True True True False,
-               Stringa.Char False False True False True True True False,
-               Stringa.Char True False True False False True True False,
-               Stringa.Char False False False False False True False False,
-               Stringa.Char False False False False True True True False,
-               Stringa.Char False True False False True True True False,
-               Stringa.Char True True True True False True True False,
-               Stringa.Char False True False False False True True False,
-               Stringa.Char False False True True False True True False,
-               Stringa.Char True False True False False True True False,
-               Stringa.Char True False True True False True True False])
+           (Str.implode
+             [Str.Char False False True False False False True False,
+               Str.Char True False False True False True True False,
+               Str.Char True True False False True True True False,
+               Str.Char False False False False True True True False,
+               Str.Char True False True False True True True False,
+               Str.Char False False True False True True True False,
+               Str.Char True False True False False True True False,
+               Str.Char False False False False False True False False,
+               Str.Char False False False False True True True False,
+               Str.Char False True False False True True True False,
+               Str.Char True True True True False True True False,
+               Str.Char False True False False False True True False,
+               Str.Char False False True True False True True False,
+               Str.Char True False True False False True True False,
+               Str.Char True False True True False True True False])
            seller)
          Arith.zero_int]
       (),
@@ -349,20 +349,20 @@ confirmClaimTransactions =
         Arith.Int_of_integer (1664822400000 :: Integer))
       [SemanticsTypes.IChoice
          (SemanticsTypes.ChoiceId
-           (Stringa.implode
-             [Stringa.Char True True False False False False True False,
-               Stringa.Char True True True True False True True False,
-               Stringa.Char False True True True False True True False,
-               Stringa.Char False True True False False True True False,
-               Stringa.Char True False False True False True True False,
-               Stringa.Char False True False False True True True False,
-               Stringa.Char True False True True False True True False,
-               Stringa.Char False False False False False True False False,
-               Stringa.Char True True False False False True True False,
-               Stringa.Char False False True True False True True False,
-               Stringa.Char True False False False False True True False,
-               Stringa.Char True False False True False True True False,
-               Stringa.Char True False True True False True True False])
+           (Str.implode
+             [Str.Char True True False False False False True False,
+               Str.Char True True True True False True True False,
+               Str.Char False True True True False True True False,
+               Str.Char False True True False False True True False,
+               Str.Char True False False True False True True False,
+               Str.Char False True False False True True True False,
+               Str.Char True False True True False True True False,
+               Str.Char False False False False False True False False,
+               Str.Char True True False False False True True False,
+               Str.Char False False True True False True True False,
+               Str.Char True False False False False True True False,
+               Str.Char True False False True False True True False,
+               Str.Char True False True True False True True False])
            mediator)
          Arith.one_int]
       ()];
@@ -380,21 +380,21 @@ dismissClaimTransactions =
         Arith.Int_of_integer (1664813100000 :: Integer))
       [SemanticsTypes.IChoice
          (SemanticsTypes.ChoiceId
-           (Stringa.implode
-             [Stringa.Char False True False False True False True False,
-               Stringa.Char True False True False False True True False,
-               Stringa.Char False False False False True True True False,
-               Stringa.Char True True True True False True True False,
-               Stringa.Char False True False False True True True False,
-               Stringa.Char False False True False True True True False,
-               Stringa.Char False False False False False True False False,
-               Stringa.Char False False False False True True True False,
-               Stringa.Char False True False False True True True False,
-               Stringa.Char True True True True False True True False,
-               Stringa.Char False True False False False True True False,
-               Stringa.Char False False True True False True True False,
-               Stringa.Char True False True False False True True False,
-               Stringa.Char True False True True False True True False])
+           (Str.implode
+             [Str.Char False True False False True False True False,
+               Str.Char True False True False False True True False,
+               Str.Char False False False False True True True False,
+               Str.Char True True True True False True True False,
+               Str.Char False True False False True True True False,
+               Str.Char False False True False True True True False,
+               Str.Char False False False False False True False False,
+               Str.Char False False False False True True True False,
+               Str.Char False True False False True True True False,
+               Str.Char True True True True False True True False,
+               Str.Char False True False False False True True False,
+               Str.Char False False True True False True True False,
+               Str.Char True False True False False True True False,
+               Str.Char True False True True False True True False])
            buyer)
          Arith.one_int]
       (),
@@ -403,22 +403,22 @@ dismissClaimTransactions =
         Arith.Int_of_integer (1664817400000 :: Integer))
       [SemanticsTypes.IChoice
          (SemanticsTypes.ChoiceId
-           (Stringa.implode
-             [Stringa.Char False False True False False False True False,
-               Stringa.Char True False False True False True True False,
-               Stringa.Char True True False False True True True False,
-               Stringa.Char False False False False True True True False,
-               Stringa.Char True False True False True True True False,
-               Stringa.Char False False True False True True True False,
-               Stringa.Char True False True False False True True False,
-               Stringa.Char False False False False False True False False,
-               Stringa.Char False False False False True True True False,
-               Stringa.Char False True False False True True True False,
-               Stringa.Char True True True True False True True False,
-               Stringa.Char False True False False False True True False,
-               Stringa.Char False False True True False True True False,
-               Stringa.Char True False True False False True True False,
-               Stringa.Char True False True True False True True False])
+           (Str.implode
+             [Str.Char False False True False False False True False,
+               Str.Char True False False True False True True False,
+               Str.Char True True False False True True True False,
+               Str.Char False False False False True True True False,
+               Str.Char True False True False True True True False,
+               Str.Char False False True False True True True False,
+               Str.Char True False True False False True True False,
+               Str.Char False False False False False True False False,
+               Str.Char False False False False True True True False,
+               Str.Char False True False False True True True False,
+               Str.Char True True True True False True True False,
+               Str.Char False True False False False True True False,
+               Str.Char False False True True False True True False,
+               Str.Char True False True False False True True False,
+               Str.Char True False True True False True True False])
            seller)
          Arith.zero_int]
       (),
@@ -427,20 +427,20 @@ dismissClaimTransactions =
         Arith.Int_of_integer (1664822400000 :: Integer))
       [SemanticsTypes.IChoice
          (SemanticsTypes.ChoiceId
-           (Stringa.implode
-             [Stringa.Char False False True False False False True False,
-               Stringa.Char True False False True False True True False,
-               Stringa.Char True True False False True True True False,
-               Stringa.Char True False True True False True True False,
-               Stringa.Char True False False True False True True False,
-               Stringa.Char True True False False True True True False,
-               Stringa.Char True True False False True True True False,
-               Stringa.Char False False False False False True False False,
-               Stringa.Char True True False False False True True False,
-               Stringa.Char False False True True False True True False,
-               Stringa.Char True False False False False True True False,
-               Stringa.Char True False False True False True True False,
-               Stringa.Char True False True True False True True False])
+           (Str.implode
+             [Str.Char False False True False False False True False,
+               Str.Char True False False True False True True False,
+               Str.Char True True False False True True True False,
+               Str.Char True False True True False True True False,
+               Str.Char True False False True False True True False,
+               Str.Char True True False False True True True False,
+               Str.Char True True False False True True True False,
+               Str.Char False False False False False True False False,
+               Str.Char True True False False False True True False,
+               Str.Char False False True True False True True False,
+               Str.Char True False False False False True True False,
+               Str.Char True False False True False True True False,
+               Str.Char True False True True False True True False])
            mediator)
          Arith.zero_int]
       ()];
@@ -458,21 +458,21 @@ confirmProblemTransactions =
         Arith.Int_of_integer (1664813100000 :: Integer))
       [SemanticsTypes.IChoice
          (SemanticsTypes.ChoiceId
-           (Stringa.implode
-             [Stringa.Char False True False False True False True False,
-               Stringa.Char True False True False False True True False,
-               Stringa.Char False False False False True True True False,
-               Stringa.Char True True True True False True True False,
-               Stringa.Char False True False False True True True False,
-               Stringa.Char False False True False True True True False,
-               Stringa.Char False False False False False True False False,
-               Stringa.Char False False False False True True True False,
-               Stringa.Char False True False False True True True False,
-               Stringa.Char True True True True False True True False,
-               Stringa.Char False True False False False True True False,
-               Stringa.Char False False True True False True True False,
-               Stringa.Char True False True False False True True False,
-               Stringa.Char True False True True False True True False])
+           (Str.implode
+             [Str.Char False True False False True False True False,
+               Str.Char True False True False False True True False,
+               Str.Char False False False False True True True False,
+               Str.Char True True True True False True True False,
+               Str.Char False True False False True True True False,
+               Str.Char False False True False True True True False,
+               Str.Char False False False False False True False False,
+               Str.Char False False False False True True True False,
+               Str.Char False True False False True True True False,
+               Str.Char True True True True False True True False,
+               Str.Char False True False False False True True False,
+               Str.Char False False True True False True True False,
+               Str.Char True False True False False True True False,
+               Str.Char True False True True False True True False])
            buyer)
          Arith.one_int]
       (),
@@ -481,22 +481,22 @@ confirmProblemTransactions =
         Arith.Int_of_integer (1664817400000 :: Integer))
       [SemanticsTypes.IChoice
          (SemanticsTypes.ChoiceId
-           (Stringa.implode
-             [Stringa.Char True True False False False False True False,
-               Stringa.Char True True True True False True True False,
-               Stringa.Char False True True True False True True False,
-               Stringa.Char False True True False False True True False,
-               Stringa.Char True False False True False True True False,
-               Stringa.Char False True False False True True True False,
-               Stringa.Char True False True True False True True False,
-               Stringa.Char False False False False False True False False,
-               Stringa.Char False False False False True True True False,
-               Stringa.Char False True False False True True True False,
-               Stringa.Char True True True True False True True False,
-               Stringa.Char False True False False False True True False,
-               Stringa.Char False False True True False True True False,
-               Stringa.Char True False True False False True True False,
-               Stringa.Char True False True True False True True False])
+           (Str.implode
+             [Str.Char True True False False False False True False,
+               Str.Char True True True True False True True False,
+               Str.Char False True True True False True True False,
+               Str.Char False True True False False True True False,
+               Str.Char True False False True False True True False,
+               Str.Char False True False False True True True False,
+               Str.Char True False True True False True True False,
+               Str.Char False False False False False True False False,
+               Str.Char False False False False True True True False,
+               Str.Char False True False False True True True False,
+               Str.Char True True True True False True True False,
+               Str.Char False True False False False True True False,
+               Str.Char False False True True False True True False,
+               Str.Char True False True False False True True False,
+               Str.Char True False True True False True True False])
            seller)
          Arith.one_int]
       ()];
@@ -519,28 +519,28 @@ everythingIsAlrightTransactions =
         Arith.Int_of_integer (1664813100000 :: Integer))
       [SemanticsTypes.IChoice
          (SemanticsTypes.ChoiceId
-           (Stringa.implode
-             [Stringa.Char True False True False False False True False,
-               Stringa.Char False True True False True True True False,
-               Stringa.Char True False True False False True True False,
-               Stringa.Char False True False False True True True False,
-               Stringa.Char True False False True True True True False,
-               Stringa.Char False False True False True True True False,
-               Stringa.Char False False False True False True True False,
-               Stringa.Char True False False True False True True False,
-               Stringa.Char False True True True False True True False,
-               Stringa.Char True True True False False True True False,
-               Stringa.Char False False False False False True False False,
-               Stringa.Char True False False True False True True False,
-               Stringa.Char True True False False True True True False,
-               Stringa.Char False False False False False True False False,
-               Stringa.Char True False False False False True True False,
-               Stringa.Char False False True True False True True False,
-               Stringa.Char False True False False True True True False,
-               Stringa.Char True False False True False True True False,
-               Stringa.Char True True True False False True True False,
-               Stringa.Char False False False True False True True False,
-               Stringa.Char False False True False True True True False])
+           (Str.implode
+             [Str.Char True False True False False False True False,
+               Str.Char False True True False True True True False,
+               Str.Char True False True False False True True False,
+               Str.Char False True False False True True True False,
+               Str.Char True False False True True True True False,
+               Str.Char False False True False True True True False,
+               Str.Char False False False True False True True False,
+               Str.Char True False False True False True True False,
+               Str.Char False True True True False True True False,
+               Str.Char True True True False False True True False,
+               Str.Char False False False False False True False False,
+               Str.Char True False False True False True True False,
+               Str.Char True True False False True True True False,
+               Str.Char False False False False False True False False,
+               Str.Char True False False False False True True False,
+               Str.Char False False True True False True True False,
+               Str.Char False True False False True True True False,
+               Str.Char True False False True False True True False,
+               Str.Char True True True False False True True False,
+               Str.Char False False False True False True True False,
+               Str.Char False False True False True True True False])
            buyer)
          Arith.zero_int]
       ()];
diff --git a/isabelle/generated/Examples/Swap.hs b/isabelle/generated/Examples/Swap.hs
index 46ee4803..09e73988 100644
--- a/isabelle/generated/Examples/Swap.hs
+++ b/isabelle/generated/Examples/Swap.hs
@@ -14,7 +14,7 @@ import Prelude ((==), (/=), (<), (<=), (>=), (>), (+), (-), (*), (/), (**),
   String, Bool(True, False), Maybe(Nothing, Just));
 import qualified Prelude;
 import qualified Semantics;
-import qualified Stringa;
+import qualified Str;
 import qualified SemanticsTypes;
 import qualified Arith;
 
@@ -59,62 +59,62 @@ swap p1 p2 =
       (makePayment p1 p2 (makePayment p2 p1 SemanticsTypes.Close)));
 
 adaToken :: SemanticsTypes.Token;
-adaToken = SemanticsTypes.Token (Stringa.implode []) (Stringa.implode []);
+adaToken = SemanticsTypes.Token (Str.implode []) (Str.implode []);
 
 adaProvider :: SemanticsTypes.Party;
 adaProvider =
   SemanticsTypes.Role
-    (Stringa.implode
-      [Stringa.Char True False False False False False True False,
-        Stringa.Char False False True False False True True False,
-        Stringa.Char True False False False False True True False,
-        Stringa.Char False False False False False True False False,
-        Stringa.Char False False False False True False True False,
-        Stringa.Char False True False False True True True False,
-        Stringa.Char True True True True False True True False,
-        Stringa.Char False True True False True True True False,
-        Stringa.Char True False False True False True True False,
-        Stringa.Char False False True False False True True False,
-        Stringa.Char True False True False False True True False,
-        Stringa.Char False True False False True True True False]);
+    (Str.implode
+      [Str.Char True False False False False False True False,
+        Str.Char False False True False False True True False,
+        Str.Char True False False False False True True False,
+        Str.Char False False False False False True False False,
+        Str.Char False False False False True False True False,
+        Str.Char False True False False True True True False,
+        Str.Char True True True True False True True False,
+        Str.Char False True True False True True True False,
+        Str.Char True False False True False True True False,
+        Str.Char False False True False False True True False,
+        Str.Char True False True False False True True False,
+        Str.Char False True False False True True True False]);
 
 dollarToken :: SemanticsTypes.Token;
 dollarToken =
   SemanticsTypes.Token
-    (Stringa.implode
-      [Stringa.Char False False False True True True False False,
-        Stringa.Char True False True False True True False False,
-        Stringa.Char False True False False False True True False,
-        Stringa.Char False True False False False True True False,
-        Stringa.Char False True True False True True False False,
-        Stringa.Char True False True False True True False False])
-    (Stringa.implode
-      [Stringa.Char False False True False False True True False,
-        Stringa.Char True True True True False True True False,
-        Stringa.Char False False True True False True True False,
-        Stringa.Char False False True True False True True False,
-        Stringa.Char True False False False False True True False,
-        Stringa.Char False True False False True True True False]);
+    (Str.implode
+      [Str.Char False False False True True True False False,
+        Str.Char True False True False True True False False,
+        Str.Char False True False False False True True False,
+        Str.Char False True False False False True True False,
+        Str.Char False True True False True True False False,
+        Str.Char True False True False True True False False])
+    (Str.implode
+      [Str.Char False False True False False True True False,
+        Str.Char True True True True False True True False,
+        Str.Char False False True True False True True False,
+        Str.Char False False True True False True True False,
+        Str.Char True False False False False True True False,
+        Str.Char False True False False True True True False]);
 
 dollarProvider :: SemanticsTypes.Party;
 dollarProvider =
   SemanticsTypes.Role
-    (Stringa.implode
-      [Stringa.Char False False True False False False True False,
-        Stringa.Char True True True True False True True False,
-        Stringa.Char False False True True False True True False,
-        Stringa.Char False False True True False True True False,
-        Stringa.Char True False False False False True True False,
-        Stringa.Char False True False False True True True False,
-        Stringa.Char False False False False False True False False,
-        Stringa.Char False False False False True False True False,
-        Stringa.Char False True False False True True True False,
-        Stringa.Char True True True True False True True False,
-        Stringa.Char False True True False True True True False,
-        Stringa.Char True False False True False True True False,
-        Stringa.Char False False True False False True True False,
-        Stringa.Char True False True False False True True False,
-        Stringa.Char False True False False True True True False]);
+    (Str.implode
+      [Str.Char False False True False False False True False,
+        Str.Char True True True True False True True False,
+        Str.Char False False True True False True True False,
+        Str.Char False False True True False True True False,
+        Str.Char True False False False False True True False,
+        Str.Char False True False False True True True False,
+        Str.Char False False False False False True False False,
+        Str.Char False False False False True False True False,
+        Str.Char False True False False True True True False,
+        Str.Char True True True True False True True False,
+        Str.Char False True True False True True True False,
+        Str.Char True False False True False True True False,
+        Str.Char False False True False False True True False,
+        Str.Char True False True False False True True False,
+        Str.Char False True False False True True True False]);
 
 swapExample :: SemanticsTypes.Contract;
 swapExample =
diff --git a/isabelle/generated/Stringa.hs b/isabelle/generated/Str.hs
similarity index 96%
rename from isabelle/generated/Stringa.hs
rename to isabelle/generated/Str.hs
index cafdc1b5..9c698c9c 100644
--- a/isabelle/generated/Stringa.hs
+++ b/isabelle/generated/Str.hs
@@ -1,6 +1,6 @@
 {-# LANGUAGE EmptyDataDecls, RankNTypes, ScopedTypeVariables #-}
 
-module Stringa(Char(..), implode) where {
+module Str(Char(..), implode) where {
 
 import Prelude ((==), (/=), (<), (<=), (>=), (>), (+), (-), (*), (/), (**),
   (>>=), (>>), (=<<), (&&), (||), (^), (^^), (.), ($), ($!), (++), (!!), Eq,
diff --git a/isabelle/marlowe.cabal b/isabelle/marlowe.cabal
index 3dddc1a9..46456491 100644
--- a/isabelle/marlowe.cabal
+++ b/isabelle/marlowe.cabal
@@ -33,7 +33,7 @@ library
         Product_Lexorder
         Product_Type
         SList
-        Stringa
+        Str
     exposed-modules:
         Arith
         ArithNumInstance
diff --git a/nix/scripts.nix b/nix/scripts.nix
index 5e81f48a..67b73e74 100644
--- a/nix/scripts.nix
+++ b/nix/scripts.nix
@@ -37,4 +37,8 @@
     cd isabelle
     isabelle jedit -d . -u Doc/Specification/Specification.thy
   '';
+  vscode-marlowe-proofs = writeShellScriptBinInRepoRoot "vscode-marlowe-proofs" ''
+    cd isabelle
+    isabelle vscode  -o "editor_output_state=true" -d . -u Doc/Specification/Specification.thy .
+  '';
 }