diff options
| author | Thomas Bauereiss <tb592@cl.cam.ac.uk> | 2019-07-26 13:10:13 +0100 |
|---|---|---|
| committer | Thomas Bauereiss <tb592@cl.cam.ac.uk> | 2019-07-26 13:11:00 +0100 |
| commit | c87bb2ccbabb4a3a7003af3913f4525ebdcc6156 (patch) | |
| tree | 19cf07880b8213af369680db5ba754a354223a24 /prover_snapshots | |
| parent | 57612b620ad2a3e1d532f24b89c29397d5af3f82 (diff) | |
| download | sail-riscv-c87bb2ccbabb4a3a7003af3913f4525ebdcc6156.zip sail-riscv-c87bb2ccbabb4a3a7003af3913f4525ebdcc6156.tar.gz sail-riscv-c87bb2ccbabb4a3a7003af3913f4525ebdcc6156.tar.bz2 | |
Fix HOL4 snapshot for recent versions of HOL4
Also fix "clean" target in Holmakefile
Diffstat (limited to 'prover_snapshots')
| -rw-r--r-- | prover_snapshots/hol4/lib/lem/lemScript.sml | 2 | ||||
| -rw-r--r-- | prover_snapshots/hol4/lib/sail/Holmakefile | 4 |
2 files changed, 2 insertions, 4 deletions
diff --git a/prover_snapshots/hol4/lib/lem/lemScript.sml b/prover_snapshots/hol4/lib/lem/lemScript.sml index d6bb1bc..94a8682 100644 --- a/prover_snapshots/hol4/lib/lem/lemScript.sml +++ b/prover_snapshots/hol4/lib/lem/lemScript.sml @@ -199,7 +199,7 @@ val _ = computeLib.add_persistent_funs ["FMAP_TO_SET_FUPDATE"] val IN_FMAP_TO_SET = store_thm ("IN_FMAP_TO_SET", - ``(k, v) IN FMAP_TO_SET m = (FLOOKUP m k = SOME v)``, + ``((k, v) IN FMAP_TO_SET m) = (FLOOKUP m k = SOME v)``, SIMP_TAC (std_ss++PRED_SET_ss) [FMAP_TO_SET_def, FLOOKUP_DEF] THEN METIS_TAC[optionTheory.option_CLAUSES]) diff --git a/prover_snapshots/hol4/lib/sail/Holmakefile b/prover_snapshots/hol4/lib/sail/Holmakefile index 16babc9..344b8b7 100644 --- a/prover_snapshots/hol4/lib/sail/Holmakefile +++ b/prover_snapshots/hol4/lib/sail/Holmakefile @@ -15,11 +15,9 @@ INCLUDES = ../lem all: $(THYS) .PHONY: all -EXTRA_CLEANS = $(LEM_CLEANS) - ifdef POLY HOLHEAP = sail-heap -EXTRA_CLEANS = $(LEM_CLEANS) $(HOLHEAP) $(HOLHEAP).o +EXTRA_CLEANS = $(HOLHEAP) $(HOLHEAP).o BASE_HEAP = ../lem/lemheap |