diff -r 4f093e55beeb -r 8a1059aa01f0 src/ZF/Inductive.thy --- a/src/ZF/Inductive.thy Mon Dec 28 16:58:11 1998 +0100 +++ b/src/ZF/Inductive.thy Mon Dec 28 16:59:28 1998 +0100 @@ -1,5 +1,5 @@ (*Dummy theory to document dependencies *) -Inductive = Fixedpt + Sum + QPair + "indrule" + +Inductive = Fixedpt + Sum + QPair + end