src/ZF/Inductive.thy
author paulson
Wed Apr 02 15:25:35 1997 +0200 (1997-04-02)
changeset 2870 6d6fd10a9fdc
parent 805 96f51689cdeb
child 6053 8a1059aa01f0
permissions -rw-r--r--
Now a non-trivial theory so that require_thy can find it
lcp@578
     1
(*Dummy theory to document dependencies *)
lcp@578
     2
paulson@2870
     3
Inductive = Fixedpt + Sum + QPair + "indrule" +
paulson@2870
     4
paulson@2870
     5
end