src/ZF/Inductive.thy
changeset 2870 6d6fd10a9fdc
parent 805 96f51689cdeb
child 6053 8a1059aa01f0
     1.1 --- a/src/ZF/Inductive.thy	Wed Apr 02 15:24:42 1997 +0200
     1.2 +++ b/src/ZF/Inductive.thy	Wed Apr 02 15:25:35 1997 +0200
     1.3 @@ -1,3 +1,5 @@
     1.4  (*Dummy theory to document dependencies *)
     1.5  
     1.6 -Inductive = Fixedpt + Sum + QPair + "indrule"
     1.7 +Inductive = Fixedpt + Sum + QPair + "indrule" +
     1.8 +
     1.9 +end