src/HOL/Induct/ROOT.ML
changeset 10876 e12892e4666a
parent 10566 7ed4f5a6c63f
child 11046 b5f5942781a0
--- a/src/HOL/Induct/ROOT.ML	Fri Jan 12 11:06:50 2001 +0100
+++ b/src/HOL/Induct/ROOT.ML	Fri Jan 12 11:08:06 2001 +0100
@@ -3,6 +3,7 @@
 Examples of Inductive and Coinductive Definitions.
 *)
 
+time_use_thy "Sigma_Algebra";
 time_use_thy "Perm";
 time_use_thy "Comb";
 time_use_thy "Mutil";