src/ZF/Fin.thy
author nipkow
Mon, 19 Feb 1996 18:04:41 +0100
changeset 1515 4ed79ebab64d
parent 484 70b789956bd3
permissions -rw-r--r--
Introduced normalize_thm into HOL.ML Corrected some dependencies among Sum, Prod and mono. Extended RelPow
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
363
1180a3c5479e renaming/removal of filenames to correct case
lcp
parents:
diff changeset
     1
(*Dummy theory to document dependencies *)
1180a3c5479e renaming/removal of filenames to correct case
lcp
parents:
diff changeset
     2
484
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents: 435
diff changeset
     3
Fin = Arith + "inductive" + "equalities"