;; THIS FILE IS GENERATED
(
("check-credit-card-number" "(check-credit-card-number str)" "index.html" "index-check_002dcredit_002dcard_002dnumber-1" "")
("credit-card-number-check-digit-ok?" "(credit-card-number-check-digit-ok? str)" "index.html" "index-credit_002dcard_002dnumber_002dcheck_002ddigit_002dok_003f-2" "")
("credit-card-number-seems-ok?" "(credit-card-number-seems-ok? str)" "index.html" "index-credit_002dcard_002dnumber_002dseems_002dok_003f-3" "")
("write-formatted-credit-card-number" "(write-formatted-credit-card-number str port)" "index.html" "index-write_002dformatted_002dcredit_002dcard_002dnumber-4" "")
("formatted-credit-card-number" "(formatted-credit-card-number str)" "index.html" "index-formatted_002dcredit_002dcard_002dnumber-5" "")
)