Skip to content

Commit

Permalink
Replace "rn" by "cdm" (1)
Browse files Browse the repository at this point in the history
See issue metamath#4470:

Label changes:
* ~ffelrnd    -> ~ffelcdmd (used 1113 times)
* ~ffelrnda  -> ~ffelcdmda (used 1119 times)
* ~ffelrni     -> ~ffelcdmi (used 229 times)
* ~ffelrn      -> ~ffelcdm (used 492 times)

"cdm" added to list of abbreviations (in comment for ~conventions-labels)
  • Loading branch information
avekens committed Dec 17, 2024
1 parent 3cbce00 commit 42d7266
Show file tree
Hide file tree
Showing 2 changed files with 68,457 additions and 68,406 deletions.
4 changes: 4 additions & 0 deletions changes-set.txt
Original file line number Diff line number Diff line change
Expand Up @@ -93,6 +93,10 @@ make a github issue.)

DONE:
Date Old New Notes
17-Dec-24 ffelrnd ffelcdmd
17-Dec-24 ffelrnda ffelcdmda
17-Dec-24 ffelrni ffelcdmi
17-Dec-24 ffelrn ffelcdm
13-Dec-24 fvmptopab [same] revised - eliminated hypothesis
and deduction form antecedent
13-Dec-24 wksonproplem [same] revised - eliminated hypothesis
Expand Down
Loading

0 comments on commit 42d7266

Please sign in to comment.