From 13eb6f5aa6a5bb9c159b02dfa1cc8c1d7bfc4d3a Mon Sep 17 00:00:00 2001 From: Magnus Myreen Date: Tue, 9 Nov 2021 14:44:27 +0100 Subject: [PATCH] Fix a mistake --- .../array/compilation/proofs/lpr_arrayRamseyProofScript.sml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/examples/lpr_checker/array/compilation/proofs/lpr_arrayRamseyProofScript.sml b/examples/lpr_checker/array/compilation/proofs/lpr_arrayRamseyProofScript.sml index 97a6bb33be..cf825a7a52 100644 --- a/examples/lpr_checker/array/compilation/proofs/lpr_arrayRamseyProofScript.sml +++ b/examples/lpr_checker/array/compilation/proofs/lpr_arrayRamseyProofScript.sml @@ -121,7 +121,7 @@ Proof metis_tac[STD_streams_stderr,add_stdo_nil]>> match_mp_tac ramsey_eq>>simp[not_is_ramsey_4_17]>> match_mp_tac ramsey_lpr_correct>> - match_mp_tac (GEN_ALL check_lpr_unsat_list_sound)>> + match_mp_tac (GEN_ALL lpr_arrayProgTheory.check_lpr_unsat_list_sound)>> fs[enc_def]>> asm_exists_tac>>simp[]>> CONJ_TAC >- (