doc-src/Tutorial/Recdef/end
author berghofe
Fri, 31 Aug 2001 16:29:18 +0200
changeset 11534 0494d0347f18
parent 6100 40d66bc3e83f
permissions -rw-r--r--
Proof of True_implies_equals is stored with "open" derivation to facilitate simplification of proof terms.

end