| changeset 67350 | f061129d891b |
| parent 62392 | 747d36865c2c |
| child 67406 | 23307fd33906 |
--- 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: