doc-src/Tutorial/Misc/Itrev.thy
changeset 5377 efb799c5ed3c
equal deleted inserted replaced
5376:60b31a24f1a6 5377:efb799c5ed3c
       
     1 Itrev = Main +
       
     2 consts itrev :: 'a list => 'a list => 'a list
       
     3 primrec
       
     4 "itrev []     ys = ys"
       
     5 "itrev (x#xs) ys = itrev xs (x#ys)"
       
     6 end