src/ZF/Fin.thy
author wenzelm
Sat, 24 Oct 1998 20:22:45 +0200
changeset 5764 ea464976a00f
parent 484 70b789956bd3
permissions -rw-r--r--
records; tuned datatype, inductive, primrec;

(*Dummy theory to document dependencies *)

Fin = Arith + "inductive" + "equalities"