diff -r b2ff1902420f -r 06ec8abfd3bc test/Tools/isac/ADDTESTS/course/phst11/T2_Rewriting.thy --- a/test/Tools/isac/ADDTESTS/course/phst11/T2_Rewriting.thy Wed Jan 11 09:23:18 2023 +0100 +++ b/test/Tools/isac/ADDTESTS/course/phst11/T2_Rewriting.thy Wed Jan 11 11:38:01 2023 +0100 @@ -68,7 +68,8 @@ http://isabelle.in.tum.de/dist/library/HOL/HOL-Multivariate_Analysis/Derivative.html \ ML \ -val t = @{term "%x. x^2 + x + y"}; TermC.atomwy t; UnparseC.term t; +val t = @{term "%x. x^2 + x + y"}; +TermC.atom_write_detail @{context} t; UnparseC.term_in_ctxt @{context} t; \ text \Since this notation does not conform to present high-school matheatics ISAC introduced the 'bdv' mechanism. This mechanism is also used for equation