author | blanchet |
Tue, 19 Mar 2024 13:24:22 +0100 | |
changeset 79930 | 7bac6bd83cc3 |
parent 79929 | 08b83f91a1b2 |
child 79931 | f08e5a234c1b |
child 79937 | d26c53bc6ce1 |
--- a/src/HOL/Real_Asymp/multiseries_expansion.ML Tue Mar 19 00:42:09 2024 +0100 +++ b/src/HOL/Real_Asymp/multiseries_expansion.ML Tue Mar 19 13:24:22 2024 +0100 @@ -1627,7 +1627,7 @@ val _ = if get_verbose ectxt then writeln "Unsupported occurrence of arctan" else () in - raise TERM ("Unsupported occurence of arctan", []) + raise TERM ("Unsupported occurrence of arctan", []) end) | _ => raise TERM ("Unexpected trim result during expansion of arctan", []) end