Fix another proof

CakeML · Nov 26, 2017 · 33fd129 · 33fd129
1 parent 3931533
commit 33fd129
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 4 deletions.
diff --git a/compiler/bootstrap/translation/to_word32ProgScript.sml b/compiler/bootstrap/translation/to_word32ProgScript.sml
@@ -427,10 +427,10 @@ val assign_rw = Q.prove(`
   rw[]
   >-
     (`0 ≤ 4* -i` by intLib.COOPER_TAC>>
-    fs[GSYM integerTheory.INT_ABS_EQ_ID])
+    metis_tac[integerTheory.INT_ABS_EQ_ID])
   >>
     `0 ≤ 4*i` by intLib.COOPER_TAC>>
-    fs[GSYM integerTheory.INT_ABS_EQ_ID])
+    metis_tac[integerTheory.INT_ABS_EQ_ID])
 
 (* TODO: word_mul should maybe target a real op ?
    TODO: econv might be going too far with case simplification

diff --git a/compiler/bootstrap/translation/to_word64ProgScript.sml b/compiler/bootstrap/translation/to_word64ProgScript.sml
@@ -429,10 +429,10 @@ val assign_rw = Q.prove(`
   rw[]
   >-
     (`0 ≤ 4* -i` by intLib.COOPER_TAC>>
-    fs[GSYM integerTheory.INT_ABS_EQ_ID])
+    metis_tac[integerTheory.INT_ABS_EQ_ID])
   >>
     `0 ≤ 4*i` by intLib.COOPER_TAC>>
-    fs[GSYM integerTheory.INT_ABS_EQ_ID])
+    metis_tac[integerTheory.INT_ABS_EQ_ID])
 
 (* TODO: word_mul should maybe target a real op ?
    TODO: econv might be going too far with case simplification