Permalink
Browse files

Remove unnecessary AC ADD_COMM ADD_ASSOC

Not only unnecessary, but after HOL-Theorem-Prover/HOL#473 was sending the simplifier into a loop.
  • Loading branch information...
xrchz committed Oct 12, 2017
1 parent 8dddb48 commit 215cc4bfdd90ff496ccf6848ac1929740d53b2bc
Showing with 1 addition and 1 deletion.
  1. +1 −1 compiler/backend/clos_to_bvlScript.sml
@@ -429,7 +429,7 @@ val compile_exps_acc = Q.store_thm("compile_exps_acc",
(LENGTH c = LENGTH xs) /\ ?ys. aux1 = ys ++ aux`,
recInduct compile_exps_ind \\ REPEAT STRIP_TAC
\\ fs [compile_exps_def] \\ SRW_TAC [] [] \\ fs [LET_DEF,ADD1]
\\ fs [AC ADD_COMM ADD_ASSOC]
\\ fs []
\\ BasicProvers.EVERY_CASE_TAC \\ rfs [] \\ fs [pair_lem1] >>
rw [] >>
fs [pair_lem2] >>

0 comments on commit 215cc4b

Please sign in to comment.