diff --git a/examples/bot/MonitorProofScript.sml b/examples/bot/MonitorProofScript.sml
index 90b34f0066..0118e176d9 100644
--- a/examples/bot/MonitorProofScript.sml
+++ b/examples/bot/MonitorProofScript.sml
@@ -1373,7 +1373,8 @@ Theorem stop_spec:
     (IOBOT w)
     (POSTv bv.
     IOBOT w *
-    &BOOL (w.wo.stop_oracle 0) bv)`,
+    &BOOL (w.wo.stop_oracle 0) bv)
+Proof
   rw [IOBOT_def] \\ qpat_abbrev_tac `Q = $POSTv _`
   \\ simp [bot_ffi_part_def, IOx_def, IO_def]
   \\ xpull \\ qunabbrev_tac `Q` >>
@@ -1411,7 +1412,8 @@ Theorem stop_spec:
   qexists_tac`b`>>
   qexists_tac`WORD8`>>simp[Abbr`b`]>>rw[]>>
   simp[ml_translatorTheory.EqualityType_NUM_BOOL]>>
-  simp[IOBOT_def]>>xsimpl);
+  simp[IOBOT_def]>>xsimpl
+QED
 
 (* eventually on oracle sequences *)
 Definition eventually_def:
diff --git a/pancake/proofs/crep_to_loopProofScript.sml b/pancake/proofs/crep_to_loopProofScript.sml
index 59715b08dd..079ec6ac8c 100644
--- a/pancake/proofs/crep_to_loopProofScript.sml
+++ b/pancake/proofs/crep_to_loopProofScript.sml
@@ -3017,7 +3017,7 @@ Proof
   >- (
     (* general call case *)
     rw []
-    \\ qmatch_goalsub_abbrev_tac ‘domain l SUBSET rhs`
+    \\ qmatch_goalsub_abbrev_tac ‘domain l SUBSET rhs’
     \\ reverse (qsuff_tac `domain l SUBSET rhs`)
     >- (
       fs [Abbr `rhs`]
diff --git a/tutorial/wordfreqProgScript.sml b/tutorial/wordfreqProgScript.sml
index 308e726222..9d563acf03 100644
--- a/tutorial/wordfreqProgScript.sml
+++ b/tutorial/wordfreqProgScript.sml
@@ -260,7 +260,7 @@ Theorem wordfreq_spec:
   (* EXERCISE: write the specification for the wordfreq program *)
   (* hint: it should be very similar to wordcount_spec (in wordcountProgScript.sml) *)
   (* hint: use wordfreq_output_spec to produce the desired output *)
-
+Proof
 (* The following proof sketch should work when you have roughly the right
    specification