From 3307d9840e93caaed0969c033bf55b654361b12a Mon Sep 17 00:00:00 2001 From: Michael Norrish Date: Wed, 3 Jul 2019 16:31:06 +1000 Subject: [PATCH] Fix examples/array_searchProg for HOL's change to MEM_DROP thms --- examples/array_searchProgScript.sml | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/examples/array_searchProgScript.sml b/examples/array_searchProgScript.sml index 4a4b135f9b..d0c7d57085 100644 --- a/examples/array_searchProgScript.sml +++ b/examples/array_searchProgScript.sml @@ -638,10 +638,7 @@ Proof [`value_v`, `EL mid elems`, `EL mid elem_vs`] mp_tac) >> fs[] >> strip_tac >> metis_tac[]) >> - (qspecl_then [`start`, `TAKE finish elems`] - mp_tac) MEM_DROP >> - impl_tac >> fs[LENGTH_TAKE] >> - rw[] >> metis_tac[] + metis_tac[MEM_DROP_IMP] ) >- (first_x_assum match_mp_tac >> fs[] >> (qspecl_then [`TAKE finish elems`, `start`,