diff options
| author | Brian Campbell | 2021-03-24 18:11:08 +0000 |
|---|---|---|
| committer | Brian Campbell | 2021-03-24 18:11:08 +0000 |
| commit | 1cb28eeb9289624b6f187705fe20e6176ccf1406 (patch) | |
| tree | 8e4fb4090b77333d78116b7c37abbd75ea787f91 /lib | |
| parent | 3ac7babbba68d64b8d54154b36d70a305955170b (diff) | |
Fix lemma for current HOL4
(should also work for older versions)
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/hol/sail2_valuesAuxiliaryScript.sml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/lib/hol/sail2_valuesAuxiliaryScript.sml b/lib/hol/sail2_valuesAuxiliaryScript.sml index b475c5ea..d35efacd 100644 --- a/lib/hol/sail2_valuesAuxiliaryScript.sml +++ b/lib/hol/sail2_valuesAuxiliaryScript.sml @@ -125,9 +125,8 @@ val just_list_spec = store_thm("just_list_spec", conj_tac \\ ho_match_mp_tac just_list_ind \\ Cases \\ rw[] - \\ rw[Once just_list_def] + \\ srw_tac [boolSimps.NORMEQ_ss] [Once just_list_def] >- ( CASE_TAC \\ fs[] \\ CASE_TAC ) - >- PROVE_TAC[] \\ Cases_on`es` \\ fs[] \\ CASE_TAC \\ fs[] \\ CASE_TAC \\ fs[] |