# HG changeset patch # User nipkow # Date 1515275752 -3600 # Node ID f061129d891b4938911dcd5a74cf928a2d70ee38 # Parent 0441f2f1b574e27fa367f7371a5ca67fbcd448a2 corrected op diff -r 0441f2f1b574 -r f061129d891b src/Doc/Tutorial/Misc/simp.thy --- 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: