From 2875e0cbdd7bba461a4d893a0a38f34c73a63b2c Mon Sep 17 00:00:00 2001 From: Magnus Myreen Date: Thu, 4 Apr 2024 04:08:47 +0200 Subject: [PATCH] Use cv_trans instead of cv_trans_pre in a few places --- src/num/theories/cv_compute/automation/cv_stdScript.sml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/num/theories/cv_compute/automation/cv_stdScript.sml b/src/num/theories/cv_compute/automation/cv_stdScript.sml index 88c67c5970..6e47d62b92 100644 --- 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 = [] /\