author  paulson 
Wed, 02 Apr 1997 15:25:35 +0200  
changeset 2870  6d6fd10a9fdc 
parent 805  96f51689cdeb 
child 6053  8a1059aa01f0 
permissions  rwrr 
578
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

1 
(*Dummy theory to document dependencies *) 
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

2 

2870
6d6fd10a9fdc
Now a nontrivial theory so that require_thy can find it
paulson
parents:
805
diff
changeset

3 
Inductive = Fixedpt + Sum + QPair + "indrule" + 
6d6fd10a9fdc
Now a nontrivial theory so that require_thy can find it
paulson
parents:
805
diff
changeset

4 

6d6fd10a9fdc
Now a nontrivial theory so that require_thy can find it
paulson
parents:
805
diff
changeset

5 
end 