fix cnf_xor infinite loop

CakeML · Feb 27, 2024 · 7b2d2fc · 7b2d2fc
1 parent 647a11e
commit 7b2d2fc
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/examples/xlrup_checker/cnf_xorScript.sml b/examples/xlrup_checker/cnf_xorScript.sml
@@ -290,7 +290,7 @@ Theorem print_lit_alt:
   (print_lit (Neg n) = int_to_string (#"-") (-&n))
 Proof
   rw[print_lit_def,int_to_string_thm,num_to_str_thm]>>
-  EVAL_TAC
+  simp[strcat_def,concat_def,implode_def]
 QED
 
 Theorem fromString_print_lit: