Use cv_trans instead of cv_trans_pre in a few places

HOL-Theorem-Prover · Apr 4, 2024 · 2875e0c · 2875e0c
1 parent 4d623c3
commit 2875e0c
Showing 1 changed file with 4 additions and 4 deletions.
diff --git a/src/num/theories/cv_compute/automation/cv_stdScript.sml b/src/num/theories/cv_compute/automation/cv_stdScript.sml
@@ -185,12 +185,12 @@ QED
 val all_distinct =
   ALL_DISTINCT |> DefnBase.one_line_ify NONE |> PURE_REWRITE_RULE [conj_eq_if,if_not]
 
-val res = cv_trans_pre all_distinct;
+val res = cv_trans all_distinct;
 
 val is_prefix =
   isPREFIX |> DefnBase.one_line_ify NONE |> PURE_REWRITE_RULE [conj_eq_if,if_not]
 
-val res = cv_trans_pre is_prefix;
+val res = cv_trans is_prefix;
 
 val res = cv_trans LUPDATE_DEF;
 
@@ -209,7 +209,7 @@ Proof
   \\ rename [‘_ = SOME y’] \\ PairCases_on ‘y’ \\ gvs []
 QED
 
-val res = cv_trans_pre index_of
+val res = cv_trans_pre index_of;
 
 Definition replicate_acc_def:
   replicate_acc n x acc =
@@ -248,7 +248,7 @@ Proof
   \\ gvs [UNZIP] \\ Cases_on ‘UNZIP t’ \\ gvs []
 QED
 
-val res = cv_trans_pre UNZIP_eq
+val res = cv_trans UNZIP_eq
 
 Definition genlist_def:
   genlist i f 0 = [] /\