src/Doc/Tutorial/Misc/simp.thy
changeset 67350 f061129d891b
parent 62392 747d36865c2c
child 67406 23307fd33906
equal deleted inserted replaced
67349:0441f2f1b574 67350:f061129d891b
   386 rev [] \(\equiv\) []
   386 rev [] \(\equiv\) []
   387 
   387 
   388 [1]Rewriting:
   388 [1]Rewriting:
   389 rev [] \(\equiv\) []
   389 rev [] \(\equiv\) []
   390 
   390 
   391 [1]Applying instance of rewrite rule "List.op @.append_Nil":
   391 [1]Applying instance of rewrite rule "List.append.append_Nil":
   392 [] @ ?y \(\equiv\) ?y
   392 [] @ ?y \(\equiv\) ?y
   393 
   393 
   394 [1]Rewriting:
   394 [1]Rewriting:
   395 [] @ [a] \(\equiv\) [a]
   395 [] @ [a] \(\equiv\) [a]
   396 
   396