From d78cf7f823d9a0909c478f1a37223b024c433bb4 Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Sun, 10 Nov 2024 05:53:24 +0100 Subject: [PATCH] fix parse errors --- examples/bot/MonitorProofScript.sml | 6 ++++-- pancake/proofs/crep_to_loopProofScript.sml | 2 +- tutorial/wordfreqProgScript.sml | 2 +- 3 files changed, 6 insertions(+), 4 deletions(-) diff --git a/examples/bot/MonitorProofScript.sml b/examples/bot/MonitorProofScript.sml index a9f7826afc..13be8c080d 100644 --- a/examples/bot/MonitorProofScript.sml +++ b/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` 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 45243a0483..89d2af97f3 100644 --- a/tutorial/wordfreqProgScript.sml +++ b/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