doc-src/Tutorial/ToyList/qed1
author paulson
Tue, 16 May 2000 14:07:06 +0200
changeset 8877 9d6514fcd584
parent 5377 efb799c5ed3c
permissions -rw-r--r--
new policy to simplify the use of numerals: #0 -> 0 #1 -> 1 #2 + n -> Suc (Suc n) similarly for n + #2

qed "rev_app";
Addsimps [rev_app];