# HG changeset patch # User wenzelm # Date 1532257238 -7200 # Node ID 9247996782c95aac58e7515e55b294dac41f99b4 # Parent 205749fba102de5f2ab7f65b2f06a02fad5aa905 avoid Unicode conflict with \; diff -r 205749fba102 -r 9247996782c9 src/HOL/TPTP/TPTP_Parser_Test.thy --- a/src/HOL/TPTP/TPTP_Parser_Test.thy Sat Jul 21 23:25:22 2018 +0200 +++ b/src/HOL/TPTP/TPTP_Parser_Test.thy Sun Jul 22 13:00:38 2018 +0200 @@ -30,14 +30,14 @@ Nonstandard "OTH123.p"), ("other", Nonstandard "other"), - ("AAA000£0.axiom", - Nonstandard "AAA000£0.axiom"), - ("AAA000£0.p", - Nonstandard "AAA000£0.p"), + ("AAA000\194\1630.axiom", + Nonstandard "AAA000\194\1630.axiom"), + ("AAA000\194\1630.p", + Nonstandard "AAA000\194\1630.p"), ("AAA000.0.p", Nonstandard "AAA000.0.p"), - ("AAA000£0.what", - Nonstandard "AAA000£0.what"), + ("AAA000\194\1630.what", + Nonstandard "AAA000\194\1630.what"), ("", Nonstandard "")]; in