fix parse errors

Author: digama0

examples/bot/MonitorProofScript.sml

@@ -1322,7 +1322,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` >>
@@ -1360,7 +1361,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 *)
 val eventually_def = Define`

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`]

tutorial/wordfreqProgScript.sml

@@ -253,7 +253,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