Remove unnecessary GEN_REWRITE_TACs... (SimpLHS is also unnecessary)

HOL-Theorem-Prover · Dec 11, 2023 · a93ab8a · a93ab8a
1 parent 5c2606c
commit a93ab8a
Showing 1 changed file with 2 additions and 3 deletions.
diff --git a/src/coalgebras/ltreeScript.sml b/src/coalgebras/ltreeScript.sml
@@ -696,7 +696,7 @@ End
 Theorem ltree_every_rewrite[simp] :
     ltree_every P (Branch a ts) <=> P a ts /\ every (ltree_every P) ts
 Proof
-    GEN_REWRITE_TAC (RATOR_CONV o ONCE_DEPTH_CONV) empty_rewrites [ltree_every_cases]
+    SIMP_TAC std_ss [Once ltree_every_cases]
  >> EQ_TAC >> rw []
 QED
 
@@ -758,8 +758,7 @@ Theorem ltree_finite_branching_rewrite[simp] :
     ltree_finite_branching (Branch a ts) <=>
     LFINITE ts /\ every ltree_finite_branching ts
 Proof
-    GEN_REWRITE_TAC (RATOR_CONV o ONCE_DEPTH_CONV) empty_rewrites
-      [ltree_finite_branching_cases]
+    SIMP_TAC std_ss [ltree_finite_branching_cases]
  >> EQ_TAC >> rw []
  >- rw [LFINITE_fromList]
  >- rw [every_fromList_EVERY]