diff -r 4ec8e654112f -r 2865a6618cba src/HOL/Library/Lexord.thy --- a/src/HOL/Library/Lexord.thy Thu Jun 26 17:25:29 2025 +0200 +++ b/src/HOL/Library/Lexord.thy Thu Jun 26 17:25:29 2025 +0200 @@ -173,8 +173,6 @@ instance list :: (order) order by (rule order.intro_of_class, rule ordering_orderI, fact lex.ordering) -export_code \(\) :: _ list \ _ list \ bool\ \(<) :: _ list \ _ list \ bool\ in Haskell - subsection \Non-canonical instance\ @@ -194,10 +192,4 @@ global_interpretation lex_dvd: preordering lex_dvd lex_dvd_strict by (fact dvd.preordering) -definition \example = lex_dvd [(4::int), - 7, 8] [- 8, 13, 5]\ - -export_code example in Haskell - -value example - end