doc-src/Contents
author paulson
Tue, 20 Jun 2000 11:41:07 +0200
changeset 9086 e4592e43e703
parent 8752 4c1a120647b8
child 13213 833ffcb2e92d
permissions -rw-r--r--
now setsum f A = 0 unless A is finite; proved setsum_cong

Intro Ref System Logics HOL ZF Inductive AxClass TutorialI IsarRef