Fix a Theorem-Proof-QED error now flagged by most recent HOL

CakeML · Jun 21, 2023 · ca3e595 · ca3e595
1 parent 191c21c
commit ca3e595
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/characteristic/examples/cf_examplesScript.sml b/characteristic/examples/cf_examplesScript.sml
@@ -143,7 +143,7 @@ Proof
   xcf' "is_none" \\ Cases_on `opt` \\
   fs [OPTION_TYPE_def] \\
   xmatch \\ xcon \\ xsimpl
-)
+QED
 
 val example_eq = (append_prog o process_topdecs)
   `fun example_eq x = (x = 3)`