author | nipkow |
Sat, 06 Jan 2018 22:55:52 +0100 | |
changeset 67350 | f061129d891b |
parent 67349 | 0441f2f1b574 |
child 67351 | 63d7aca15f6b |
--- a/src/Doc/Tutorial/Misc/simp.thy Sat Jan 06 17:41:21 2018 +0100 +++ b/src/Doc/Tutorial/Misc/simp.thy Sat Jan 06 22:55:52 2018 +0100 @@ -388,7 +388,7 @@ [1]Rewriting: rev [] \(\equiv\) [] -[1]Applying instance of rewrite rule "List.op @.append_Nil": +[1]Applying instance of rewrite rule "List.append.append_Nil": [] @ ?y \(\equiv\) ?y [1]Rewriting: